Theorem InnerProductGeometry.sin_angle_nonneg

Modification history

2025-02-05 22:11
Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
feat: add theorem about the norm of cross products (#20920) …
Added InnerProductGeometry.sin_angle_nonnegView on Github →