case h
𝕂 : Type u_2
𝕂' : Type u_3
𝔸 : Type u_1
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
x : 𝔸
⊢ exp 𝕂 x = exp 𝕂' x
𝕂 : Type u_2
𝕂' : Type u_3
𝔸 : Type u_1
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
⊢ exp 𝕂 = exp 𝕂'
ext x
case h
𝕂 : Type u_2
𝕂' : Type u_3
𝔸 : Type u_1
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
x : 𝔸
⊢ FormalMultilinearSeries.sum (expSeries 𝕂 𝔸) x = FormalMultilinearSeries.sum (expSeries 𝕂' 𝔸) x
case h
𝕂 : Type u_2
𝕂' : Type u_3
𝔸 : Type u_1
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
x : 𝔸
⊢ exp 𝕂 x = exp 𝕂' x
rw [exp, exp]
case h
𝕂 : Type u_2
𝕂' : Type u_3
𝔸 : Type u_1
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ (↑(expSeries 𝕂 𝔸 n) fun x_1 => x) = ↑(expSeries 𝕂' 𝔸 n) fun x_1 => x
case h
𝕂 : Type u_2
𝕂' : Type u_3
𝔸 : Type u_1
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
x : 𝔸
⊢ FormalMultilinearSeries.sum (expSeries 𝕂 𝔸) x = FormalMultilinearSeries.sum (expSeries 𝕂' 𝔸) x
refine' tsum_congr fun n => _
no goals
case h
𝕂 : Type u_2
𝕂' : Type u_3
𝔸 : Type u_1
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ (↑(expSeries 𝕂 𝔸 n) fun x_1 => x) = ↑(expSeries 𝕂' 𝔸 n) fun x_1 => x
rw [expSeries_eq_expSeries 𝕂 𝕂' 𝔸 n x]