Diff — Parabola

Revision #1982 → #2488 · back to history

modifiedParabola as focus–directrix locuseaa54cd1a850

Field	From #1982	To #2488
note	Mathlib has no notion of parabola, focus, or directrix, so the focus–directrix locus is not formalized.	Mathlib has no notion of parabola, focus, or directrix; grep for 'Parabola' in Mathlib/ returns no files.

addedMenaechmus' doubling the cube via parabolasf791c93f09e0

addedPolar of an external pole meets the parabola at tangent pointsbeec6948d058

addedTwisted cubic27b21b24fbbc

addedSuspension-bridge cable approximates a parabolae79db066705d