case h
𝕂 : Type u_3
𝔸 : Type u_2
inst✝³ : IsROrC 𝕂
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_1
s : Finset ι
f : ι → 𝔸
⊢ Set.Pairwise ↑s fun i j => Commute (f i) (f j)

case h
𝕂 : Type u_3
𝔸 : Type u_2
inst✝³ : IsROrC 𝕂
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_1
s : Finset ι
f : ι → 𝔸
⊢ Set.Pairwise ↑s fun i j => Commute (f i) (f j)
𝕂 : Type u_3
𝔸 : Type u_2
inst✝³ : IsROrC 𝕂
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_1
s : Finset ι
f : ι → 𝔸
⊢ exp 𝕂 (∑ i in s, f i) = ∏ i in s, exp 𝕂 (f i)
rw [exp_sum_of_commute, Finset.noncommProd_eq_prod]
no goals
case h
𝕂 : Type u_3
𝔸 : Type u_2
inst✝³ : IsROrC 𝕂
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_1
s : Finset ι
f : ι → 𝔸
⊢ Set.Pairwise ↑s fun i j => Commute (f i) (f j)

case h
𝕂 : Type u_3
𝔸 : Type u_2
inst✝³ : IsROrC 𝕂
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_1
s : Finset ι
f : ι → 𝔸
⊢ Set.Pairwise ↑s fun i j => Commute (f i) (f j)
exact fun i _hi j _hj _ => Commute.all _ _