𝕜 : Type u_3
R : Type u_1
M : Type u_2
inst✝¹⁷ : IsROrC 𝕜
inst✝¹⁶ : NormedRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : NormedAlgebra 𝕜 R
inst✝¹³ : Module R M
inst✝¹² : Module Rᵐᵒᵖ M
inst✝¹¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝¹⁰ : Module 𝕜 M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
⊢ (∑' (n : ℕ), ↑(expSeries 𝕜 (tsze R M) n) fun x_1 => x) =
    inl (∑' (n : ℕ), ↑(expSeries 𝕜 R n) fun x_1 => fst x) +
      inr ((∑' (n : ℕ), ↑(expSeries 𝕜 R n) fun x_1 => fst x) • snd x)
𝕜 : Type u_3
R : Type u_1
M : Type u_2
inst✝¹⁷ : IsROrC 𝕜
inst✝¹⁶ : NormedRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : NormedAlgebra 𝕜 R
inst✝¹³ : Module R M
inst✝¹² : Module Rᵐᵒᵖ M
inst✝¹¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝¹⁰ : Module 𝕜 M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
⊢ exp 𝕜 x = inl (exp 𝕜 (fst x)) + inr (exp 𝕜 (fst x) • snd x)
simp_rw [exp, FormalMultilinearSeries.sum]
𝕜 : Type u_3
R : Type u_1
M : Type u_2
inst✝¹⁷ : IsROrC 𝕜
inst✝¹⁶ : NormedRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : NormedAlgebra 𝕜 R
inst✝¹³ : Module R M
inst✝¹² : Module Rᵐᵒᵖ M
inst✝¹¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝¹⁰ : Module 𝕜 M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
⊢ HasSum (fun n => ↑(expSeries 𝕜 R n) fun x_1 => fst x) (∑' (n : ℕ), ↑(expSeries 𝕜 R n) fun x_1 => fst x)
𝕜 : Type u_3
R : Type u_1
M : Type u_2
inst✝¹⁷ : IsROrC 𝕜
inst✝¹⁶ : NormedRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : NormedAlgebra 𝕜 R
inst✝¹³ : Module R M
inst✝¹² : Module Rᵐᵒᵖ M
inst✝¹¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝¹⁰ : Module 𝕜 M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
⊢ (∑' (n : ℕ), ↑(expSeries 𝕜 (tsze R M) n) fun x_1 => x) =
    inl (∑' (n : ℕ), ↑(expSeries 𝕜 R n) fun x_1 => fst x) +
      inr ((∑' (n : ℕ), ↑(expSeries 𝕜 R n) fun x_1 => fst x) • snd x)
refine' (hasSum_expSeries_of_smul_comm 𝕜 x hx _).tsum_eq
no goals
𝕜 : Type u_3
R : Type u_1
M : Type u_2
inst✝¹⁷ : IsROrC 𝕜
inst✝¹⁶ : NormedRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : NormedAlgebra 𝕜 R
inst✝¹³ : Module R M
inst✝¹² : Module Rᵐᵒᵖ M
inst✝¹¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝¹⁰ : Module 𝕜 M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalRing R
inst✝⁵ : TopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : CompleteSpace R
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
hx : MulOpposite.op (fst x) • snd x = fst x • snd x
⊢ HasSum (fun n => ↑(expSeries 𝕜 R n) fun x_1 => fst x) (∑' (n : ℕ), ↑(expSeries 𝕜 R n) fun x_1 => fst x)
exact expSeries_hasSum_exp _