Mathlib Changelog
v4
Changelog
About
Github
Theorem
InnerProductGeometry.angle_self_neg_of_ne_zero
Modification history
2026-10-26 16:38
Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
chore: rename `nonzero` to `ne_zero` in theorem names (#44824) …
Added
InnerProductGeometry.angle_self_neg_of_ne_zero
View on Github →