Revision #1196 → #1720 · back to history
modifiedPostulate 1 (line through two points)433c9512526d
| Field | From #1196 | To #1720 |
|---|
| mathlib.module | — | Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs |
modifiedCommon notions4ba040c88987
| Field | From #1196 | To #1720 |
|---|
| mathlib.module | — | Init.Prelude |
addedVolume scales as cube of linear dimension43b65a041127
addedArchimedean propertye4fd453359fa
modifiedAffine geometry493a12cf9db3
| Field | From #1196 | To #1720 |
|---|
| note | AffineSpace (notation for AddTorsor) and a full affine geometry library exist, capturing the field but not a single 'affine geometry' statement. | AffineSpace is a scoped notation for AddTorsor and a full affine geometry library exists, capturing the field but not a single 'affine geometry' statement. |
addedImpossibility of doubling the cubee42238b46706
addedImpossibility of squaring the circled79681a97c74
modifiedLaw of contradiction29d3828c95ea
| Field | From #1196 | To #1720 |
|---|
| mathlib.module | — | Init.PropLemmas |