Theorem EuclideanGeometry.dist_orthogonalProjection_eq_of_oangle_eq

Modification history

2025-11-14 20:02
Mathlib/Geometry/Euclidean/Angle/Bisector.lean
feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection and equal distance (#30477) …
Added EuclideanGeometry.dist_orthogonalProjection_eq_of_oangle_eqView on Github →