[Merged by Bors] - feat(geometry/euclidean/angle/oriented/basic): angles and spans of vectors

[jsm28]

Add lemmas relating angles when vectors involved span the same subspace (this is preparation for corresponding lemmas in the affine case, about angles involving points on parallel lines).

---

[ocfnash]

I wonder about introducing some more support for the pattern of angles being "equal after possibly doubling" which is very common. For example what do you think of:

@[derive [normed_add_comm_group, inhabited, has_coe_t ℝ]]
def angle' : Type := add_circle π

noncomputable def real.angle.to_angle' : angle →+ angle' :=
quotient_add_group.lift
  (add_subgroup.zmultiples (2 * π))
  (quotient_add_group.mk' (add_subgroup.zmultiples π))
  sorry

example (x : angle) : x.to_angle' = 0 ↔ x = 0 ∨ x = ↑π := sorry

example (x : angle) : x.to_angle' = 0 ↔ (2 : ℤ) • x = 0 := sorry

In any case these changes look fine.

bors merge

[jsm28]

If you have an explicit type for angles mod π, I'd be concerned you probably end up with a lot of API duplication; that's why I've preferred to work consistently with angles mod 2 * π and assert things about doubling the angles when required.

If you want to define angles literally between unoriented lines - as opposed to between vectors or between oriented lines - then you do get angles mod π, but that could also reasonably be worked around by defining the angle function on lines to return twice the angle in that case (which doesn't make any difference except when you compare to constants or apply trigonometric functions), so avoiding the extra type. I don't know what exactly the French curriculum has in mind for "angles de droites" (questionably translated "angles between planes" in undergrad.yaml).

See also #17485 for more discussion of working with equality of twice angles.

[bors]

Pull request successfully merged into master.

Build succeeded:

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