English
If a^k = 0, then exp(a) equals the sum over i=0..k-1 of (i!)^{-1} a^i.
Русский
Если a^k = 0, то exp(a) равно сумме по i от 0 до k-1: (i!)^{-1} a^i.
LaTeX
$$exp(a) = \sum_{i=0}^{k-1} (i!)^{-1} a^{i} \quad\text{when } a^{k}=0$$
Lean4
theorem exp_eq_sum {a : A} {k : ℕ} (h : a ^ k = 0) : exp a = ∑ i ∈ range k, (i.factorial : ℚ)⁻¹ • (a ^ i) :=
by
have h₁ :
∑ i ∈ range k, (i.factorial : ℚ)⁻¹ • (a ^ i) =
∑ i ∈ range (nilpotencyClass a), (i.factorial : ℚ)⁻¹ • (a ^ i) +
∑ i ∈ Ico (nilpotencyClass a) k, (i.factorial : ℚ)⁻¹ • (a ^ i) :=
(sum_range_add_sum_Ico _ (csInf_le' h)).symm
suffices ∑ i ∈ Ico (nilpotencyClass a) k, (i.factorial : ℚ)⁻¹ • (a ^ i) = 0
by
dsimp [exp]
rw [h₁, this, add_zero]
exact sum_eq_zero fun _ h₂ => by rw [pow_eq_zero_of_le (mem_Ico.1 h₂).1 (pow_nilpotencyClass ⟨k, h⟩), smul_zero]
