case a
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : { x // x ∈ selfAdjoint A }
h : Commute ↑a ↑b
⊢ ↑(expUnitary (a + b)) = ↑(expUnitary a * expUnitary b)
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : { x // x ∈ selfAdjoint A }
h : Commute ↑a ↑b
⊢ expUnitary (a + b) = expUnitary a * expUnitary b
ext
case a
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : { x // x ∈ selfAdjoint A }
h : Commute ↑a ↑b
hcomm : Commute (I • ↑a) (I • ↑b)
⊢ ↑(expUnitary (a + b)) = ↑(expUnitary a * expUnitary b)
case a
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : { x // x ∈ selfAdjoint A }
h : Commute ↑a ↑b
⊢ ↑(expUnitary (a + b)) = ↑(expUnitary a * expUnitary b)
have hcomm : Commute (I • (a : A)) (I • (b : A)) := by
  unfold Commute SemiconjBy
  simp only [h.eq, Algebra.smul_mul_assoc, Algebra.mul_smul_comm]
no goals
case a
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : { x // x ∈ selfAdjoint A }
h : Commute ↑a ↑b
hcomm : Commute (I • ↑a) (I • ↑b)
⊢ ↑(expUnitary (a + b)) = ↑(expUnitary a * expUnitary b)
simpa only [expUnitary_coe, AddSubgroup.coe_add, smul_add] using exp_add_of_commute hcomm
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : { x // x ∈ selfAdjoint A }
h : Commute ↑a ↑b
⊢ I • ↑a * I • ↑b = I • ↑b * I • ↑a
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : { x // x ∈ selfAdjoint A }
h : Commute ↑a ↑b
⊢ Commute (I • ↑a) (I • ↑b)
unfold Commute SemiconjBy
no goals
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : { x // x ∈ selfAdjoint A }
h : Commute ↑a ↑b
⊢ I • ↑a * I • ↑b = I • ↑b * I • ↑a
simp only [h.eq, Algebra.smul_mul_assoc, Algebra.mul_smul_comm]