Theorem Orientation.two_zsmul_oangle_left_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_left_of_span_eq View 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_left_of_span_eq View on Github →