Theorem Orientation.two_zsmul_oangle_of_span_eq_of_span_eq

Modification history

2025-11-28 14:12
Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
feat(LinearAlgebra/Span): improve `R ∙ x` notation precedence and printing (#32108) …
Modified Orientation.two_zsmul_oangle_of_span_eq_of_span_eqView on Github →
2023-06-13 08:12
Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
feat: port Geometry.Euclidean.Angle.Oriented.Basic (#4966)
Added Orientation.two_zsmul_oangle_of_span_eq_of_span_eqView on Github →