Revision #1198 → #1821 · back to history
modifiedEuclidean space (affine)ebb4490a020b
| Field | From #1198 | To #1821 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.AffineSpace.Defs | Mathlib.Algebra.AddTorsor.Defs |
modifiedTranslation action on a point0a7e279f7c42
| Field | From #1198 | To #1821 |
|---|
| mathlib.module | Mathlib.Algebra.AddTorsor.Defs | Mathlib.Algebra.Notation.Defs |
| note | The notation `v +ᵥ P` (or `P + v` after swapping) is the `VAdd` action used in every `AddTorsor`. | The notation `v +ᵥ P` is the `VAdd` action used in every `AddTorsor`. |
modifiedVector space as Euclidean space1f8676259c82
| Field | From #1198 | To #1821 |
|---|
| mathlib.decl | AddGroup.toAddTorsor | AddGroup.instAddTorsor |
| mathlib.module | Mathlib.Algebra.AddTorsor.Defs | Mathlib.Algebra.Torsor.Defs |
modifiedLine through two points0a27977990e0
| Field | From #1198 | To #1821 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic | Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs |
addedTwo distinct lines intersect in at most one point7587a5ff88d4
modifiedTriangle inequality593ed4314ab7
| Field | From #1198 | To #1821 |
|---|
| mathlib.module | Mathlib.Topology.MetricSpace.Defs | Mathlib.Topology.MetricSpace.Pseudo.Defs |
modifiedEuclidean space is complete7794488bb1ef
| Field | From #1198 | To #1821 |
|---|
| mathlib.decl | PiLp.instCompleteSpace | PiLp.completeSpace |
modifiedOrthogonal vectors3b57ff65009f
| Field | From #1198 | To #1821 |
|---|
| mathlib.decl | inner_eq_zero_iff_angle_eq_pi_div_two | InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two |
| note | Orthogonality is just `⟪x, y⟫ = 0`; the equivalence with `angle = π/2` is `inner_eq_zero_iff_angle_eq_pi_div_two`. | Orthogonality is just `⟪x, y⟫ = 0`; the equivalence with `angle = π/2` is `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two`. |
modifiedPythagorean theoremc2d4391d338b
| Field | From #1198 | To #1821 |
|---|
| mathlib.module | Mathlib.Geometry.Euclidean.Triangle | Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle |
modifiedAffine / skew coordinates8d714073842f
| Field | From #1198 | To #1821 |
|---|
| mathlib.decl | Basis.repr | Module.Basis.repr |
| note | Skew/affine coordinates are realised via `Basis.repr` after picking an origin; not packaged separately. | Skew/affine coordinates are realised via `Module.Basis.repr` after picking an origin; not packaged separately. |
addedPolar coordinate system7b70dff0b2f9
modifiedIsometry between metric spaces6bb26b88baad
| Field | From #1198 | To #1821 |
|---|
| mathlib.module | Mathlib.Topology.MetricSpace.IsometricSMul | Mathlib.Topology.MetricSpace.Isometry |
modifiedOrigin-preserving isometry preserves norm and inner product1050b0358443
| Field | From #1198 | To #1821 |
|---|
| mathlib.module | Mathlib.Analysis.InnerProductSpace.Basic | Mathlib.Analysis.InnerProductSpace.LinearMap |
modifiedIsometry of Euclidean vector spaces is linearb7327da95a18
| Field | From #1198 | To #1821 |
|---|
| mathlib.module | Mathlib.Analysis.Normed.Affine.MazurUlam | Mathlib.Analysis.Normed.Affine.AddTorsor |
modifiedIsometric Euclidean spaces have same dimension9779d79169f0
| Field | From #1198 | To #1821 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.FiniteDimensional.Defs | Mathlib.LinearAlgebra.Dimension.Finrank |
addedEuclidean topology equals product topologyb4c6dfdff576
modifiedOpen sets via open ballsdc4d2c3c8c11
| Field | From #1198 | To #1821 |
|---|
| mathlib.module | Mathlib.Topology.MetricSpace.Defs | Mathlib.Topology.MetricSpace.Pseudo.Defs |
modifiedPseudo-Euclidean space4b867176565a
| Field | From #1198 | To #1821 |
|---|
| mathlib.decl | QuadraticForm.Nondegenerate | QuadraticMap.Nondegenerate |
| mathlib.module | Mathlib.LinearAlgebra.QuadraticForm.Basic | Mathlib.LinearAlgebra.QuadraticForm.Radical |
| note | Non-degenerate quadratic forms exist in Mathlib (`QuadraticForm.Nondegenerate`), but no named `PseudoEuclideanSpace` structure was found. | Non-degenerate quadratic forms exist in Mathlib (`QuadraticMap.Nondegenerate`), but no named `PseudoEuclideanSpace` structure was found. |