feat(analysis/normed_space/exponential): Aeᴮ = eᴮA if AB = BA (#13881)

This commit shows that the exponenential commutes if the exponent does.
This generalizes a previous weaker result.

Author: eric-wieser

src/analysis/normed_space/exponential.lean

@@ -123,6 +123,20 @@ begin
   simp [h]
 end
 
+variables (𝕂)
+
+lemma commute.exp_right [t2_space 𝔸] {x y : 𝔸} (h : commute x y) : commute x (exp 𝕂 𝔸 y) :=
+begin
+  rw exp_eq_tsum,
+  exact commute.tsum_right x (λ n, (h.pow_right n).smul_right _),
+end
+
+lemma commute.exp_left [t2_space 𝔸] {x y : 𝔸} (h : commute x y) : commute (exp 𝕂 𝔸 x) y :=
+(h.symm.exp_right 𝕂).symm
+
+lemma commute.exp [t2_space 𝔸] {x y : 𝔸} (h : commute x y) : commute (exp 𝕂 𝔸 x) (exp 𝕂 𝔸 y) :=
+(h.exp_left _).exp_right _
+
 end topological_algebra
 
 section normed
@@ -421,10 +435,6 @@ begin
   exact ring.inverse_invertible _,
 end
 
-lemma commute.exp {x y : 𝔸} (h : commute x y) :
-  commute (exp 𝕂 𝔸 x) (exp 𝕂 𝔸 y) :=
-(exp_add_of_commute h).symm.trans $ (congr_arg _ $ add_comm _ _).trans (exp_add_of_commute h.symm)
-
 end
 
 /-- In a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, if a family of elements `f i` mutually

src/topology/algebra/infinite_sum.lean

@@ -777,6 +777,15 @@ lemma summable.tsum_mul_left (a) (hf : summable f) : ∑'b, a * f b = a * ∑'b,
 lemma summable.tsum_mul_right (a) (hf : summable f) : (∑'b, f b * a) = (∑'b, f b) * a :=
 (hf.has_sum.mul_right _).tsum_eq
 
+lemma commute.tsum_right (a) (h : ∀ b, commute a (f b)) : commute a (∑' b, f b) :=
+if hf : summable f then
+  (hf.tsum_mul_left a).symm.trans ((congr_arg _ $ funext h).trans (hf.tsum_mul_right a))
+else
+  (tsum_eq_zero_of_not_summable hf).symm ▸ commute.zero_right _
+
+lemma commute.tsum_left (a) (h : ∀ b, commute (f b) a) : commute (∑' b, f b) a :=
+(commute.tsum_right _ $ λ b, (h b).symm).symm
+
 end tsum
 
 end topological_semiring