English
For a fixed nonzero natural n, the sum (1 + X + X^2 + ... + X^{n-1}) is monic when X is the indeterminate.
Русский
Для натурального n > 0 сумма иррациональных степеней (1 + X + X^2 + ... + X^{n-1}) является монической полиномиальной суммой, когда X — индентерминант.
LaTeX
$$$\bigl(\sum_{i=0}^{n-1} X^i\bigr) \text{ Monic if } n \neq 0.$$$
Lean4
theorem geom_sum_X_comp_X_add_one_eq_sum (n : ℕ) :
(∑ i ∈ range n, (X : R[X]) ^ i).comp (X + 1) =
(Finset.range n).sum fun i : ℕ => (n.choose (i + 1) : R[X]) * X ^ i :=
by
ext i
trans (n.choose (i + 1) : R); swap
· simp only [finset_sum_coeff, ← C_eq_natCast, coeff_C_mul_X_pow]
rw [Finset.sum_eq_single i, if_pos rfl]
· simp +contextual only [@eq_comm _ i, if_false, imp_true_iff]
·
simp +contextual only [Nat.lt_add_one_iff, Nat.choose_eq_zero_of_lt, Nat.cast_zero, Finset.mem_range, not_lt,
if_true, imp_true_iff]
induction n generalizing i with
| zero => dsimp; simp only [zero_comp, coeff_zero, Nat.cast_zero]
| succ n ih =>
simp only [geom_sum_succ', ih, add_comp, X_pow_comp, coeff_add, Nat.choose_succ_succ, Nat.cast_add,
coeff_X_add_one_pow]
