mathlib3

ae714fd5 - feat(geometry/euclidean/angle/oriented/basic): `rotation_rotation` (#17235)

feat(geometry/euclidean/angle/oriented/basic): `rotation_rotation` (#17235) Add another version of the lemma that rotating twice is equivalent to rotating by the sum of the angles, but for applying `rotation` twice to a vector rather than combining the isometries with `trans`.