Revision #2110 → #2804 · back to history
modifiedCurvature (intuitive)7f2bc1292cf8
| Field | From #2110 | To #2804 |
|---|
| note | No curvature concepts found in Mathlib4 (only an incidental comment mention in Mathlib/MeasureTheory/Measure/Doubling.lean). | Confirmed: only an incidental mention of the word 'curvature' appears in Mathlib/MeasureTheory/Measure/Doubling.lean; no curvature concept is defined. |
modifiedStraight lines have zero curvature645496e09938
| Field | From #2110 | To #2804 |
|---|
| note | No curvature concept (and so no zero-curvature characterization of lines) in Mathlib4. | No curvature concept (hence no zero-curvature characterization of lines) in Mathlib4. |
addedOresme's early notion of curvature5bd70ba62ab7
addedCurvature comb parametrizationa45cc1d4b5b5
addedGauss map (differential yields shape operator)69eebf5e4ed3
addedGauss curvature and mean curvature via shape operator20fa9df37f0d
addedCurvature form (holonomy generalization)0089e34defaa
addedJacobi field (sectional curvature generalization)fc7e7b38ea7a