mathlib3
217daaf4 - feat(geometry/euclidean/angle/unoriented/affine): more collinearity lemmas (#18069)

Commit
3 years ago
feat(geometry/euclidean/angle/unoriented/affine): more collinearity lemmas (#18069) These lemmas relating collinearity and angles of zero or pi are less general than the existing `collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi` from which they are deduced, but may be more convenient to use. Suggested by review of #17993.
Author
Parents
Loading