Revision #1579 → #1851 · back to history
modifiedDiameter and antipodal pointsc2a08ad26f13
| Field | From #1579 | To #1851 |
|---|
| mathlib.decl | contMDiffNegSphere | contMDiff_neg_sphere |
| note | Antipodal map on the unit sphere is formalized via negation, but diameter as a chord/segment is not defined. | The antipodal map on the unit sphere is formalized via negation (`contMDiff_neg_sphere`), but diameter as a chord/segment is not defined. |
addedArchimedes' sphere–cylinder volume relation6139208dffec
addedSurface area as derivative of volume7d9b023ec4bd
addedRotation group SO(3) acts on the sphere0e4511197f72
addedSphere fails the parallel postulatef262b09a407b
modifiedAntipodal points on the sphere5e59dff8c7af
| Field | From #1579 | To #1851 |
|---|
| mathlib.decl | contMDiffNegSphere | contMDiff_neg_sphere |
addedExotic spheree869b6caf2d3