feat(analysis/complex/isometry): `rotation_trans` (#12015)
feat(analysis/complex/isometry): `rotation_trans` (#12015)

Add a `simp` lemma about the composition of two rotations.







leanprover-community/mathlib,leanprover-community/mathlib