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

Add a `simp` lemma about the composition of two rotations.
leanprover-community · Feb 14, 2022 · 26fd61c · 26fd61c
1 parent 77dfac2
commit 26fd61c
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/analysis/complex/isometry.lean b/src/analysis/complex/isometry.lean
@@ -45,6 +45,10 @@ def rotation : circle →* (ℂ ≃ₗᵢ[ℝ] ℂ) :=
 @[simp] lemma rotation_symm (a : circle) : (rotation a).symm = rotation a⁻¹ :=
 linear_isometry_equiv.ext $ λ x, rfl
 
+@[simp] lemma rotation_trans (a b : circle) :
+  (rotation a).trans (rotation b) = rotation (b * a) :=
+by { ext1, simp }
+
 lemma rotation_ne_conj_lie (a : circle) : rotation a ≠ conj_lie :=
 begin
   intro h,