mathlib

260f0788 - feat(geometry/euclidean/angle/oriented/basic): angles and spans of vectors (#17525)

feat(geometry/euclidean/angle/oriented/basic): angles and spans of vectors (#17525) 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).