[Merged by Bors] - feat(geometry/euclidean/angle/unoriented/affine): more collinearity lemmas

[jsm28]

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.

---

[eric-wieser]

bors merge

Thanks! Can you add similar lemmas for oangle in a later PR?

[jsm28]

I've noted adding oangle variants of these lemmas on my (long) geometry todo list, which also has a more general point about ensuring oriented angle equivalents of all unoriented angle API. I might not do much from that list (beyond probably splitting up some geometry files further) before the Lean 4 conversion is complete, however; even though Euclidean geometry is a long way from the rising tide of Lean 4 conversion, affine spaces probably aren't so far away, and it's common for geometry work (in general, not these specific oangle lemmas) to involve adding some affine space lemmas.

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests