Theorem EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_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.oangle_eq_of_dist_orthogonalProjection_eqView on Github →