𝕂 : Type u_2
𝔸 : Type u_1
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
n : ℕ
⊢ (↑n !)⁻¹ • 0 ^ n = Pi.single 0 1 n
𝕂 : Type u_2
𝔸 : Type u_1
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
n : ℕ
⊢ (↑(expSeries 𝕂 𝔸 n) fun x => 0) = Pi.single 0 1 n
rw [expSeries_apply_eq]
case zero
𝕂 : Type u_2
𝔸 : Type u_1
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
⊢ (↑Nat.zero !)⁻¹ • 0 ^ Nat.zero = Pi.single 0 1 Nat.zero

case succ
𝕂 : Type u_2
𝔸 : Type u_1
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
n : ℕ
⊢ (↑(Nat.succ n)!)⁻¹ • 0 ^ Nat.succ n = Pi.single 0 1 (Nat.succ n)
𝕂 : Type u_2
𝔸 : Type u_1
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
n : ℕ
⊢ (↑n !)⁻¹ • 0 ^ n = Pi.single 0 1 n
cases' n with n
no goals
case zero
𝕂 : Type u_2
𝔸 : Type u_1
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
⊢ (↑Nat.zero !)⁻¹ • 0 ^ Nat.zero = Pi.single 0 1 Nat.zero
rw [pow_zero, Nat.factorial_zero, Nat.cast_one, inv_one, one_smul, Pi.single_eq_same]
no goals
case succ
𝕂 : Type u_2
𝔸 : Type u_1
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
n : ℕ
⊢ (↑(Nat.succ n)!)⁻¹ • 0 ^ Nat.succ n = Pi.single 0 1 (Nat.succ n)
rw [zero_pow (Nat.succ_pos _), smul_zero, Pi.single_eq_of_ne n.succ_ne_zero]