Revision #2565 → #3166 · back to history
modifiedVector space as Euclidean space1f8676259c82
| Field | From #2565 | To #3166 |
|---|
| mathlib.module | Mathlib.Algebra.Torsor.Defs | Mathlib.Algebra.AddTorsor.Defs |
| provenance | ai | ai-moderated |
addedPositive-definite symmetric bilinear form on the direction08231e41f1d0
modifiedOrthogonal vectors3b57ff65009f
| Field | From #2565 | To #3166 |
|---|
| mathlib.match_kind | exact | invocation |
| note | Orthogonality is just `⟪x, y⟫ = 0`; the equivalence with `angle = π/2` is `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two`. | Orthogonality of two vectors is just `⟪x, y⟫ = 0`; the equivalence with `angle = π/2` is `InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two`. |
| provenance | ai | ai-moderated |
addedRiemannian manifold1b87ef1af50c