Revision #3560 → #4076 · back to history
modifiedKepler's first law (lead)d11c0d0e46f3
| Field | From #3560 | To #4076 |
|---|
| note | Mathlib has no Kepler-orbit or ellipse-shaped trajectory formalization (no hits for Kepler/ellipse). | Mathlib has no Kepler-orbit or ellipse-shaped trajectory formalization (grep for Kepler/Ellipse returns nothing). |
modifiedInverse square law for planetary acceleration68a3136ca4f9
| Field | From #3560 | To #4076 |
|---|
| anchor.snippet | the acceleration vector | This means that the acceleration vector |
| provenance | ai | ai-moderated |
addedKepler enunciated the third (harmonic) law in 161989280cd58a2f
addedAngular-velocity substitution yielding Kepler's third law012835e66fa2
addedPosition vector in polar coordinates and its unit-vector decomposition4e329023a4aa
deletedKepler's equation derivation via a²/2 division8b5e8b7abb22