English
For n > 1, the constant term of Φ_n(R) is 1.
Русский
Для n > 1 константный член Φ_n(R) равен 1.
LaTeX
$$$$\text{If } 1 < n:\quad (\mathrm{cyclotomic}\ n\ R).{\text{coeff}}_{0} = 1.$$$$
Lean4
/-- The constant term of `cyclotomic n R` is `1` if `2 ≤ n`. -/
theorem cyclotomic_coeff_zero (R : Type*) [CommRing R] {n : ℕ} (hn : 1 < n) : (cyclotomic n R).coeff 0 = 1 :=
by
induction n using Nat.strong_induction_on with
| _ n hi
have hprod : (∏ i ∈ Nat.properDivisors n, (Polynomial.cyclotomic i R).coeff 0) = -1 :=
by
rw [← Finset.insert_erase (Nat.one_mem_properDivisors_iff_one_lt.2 (lt_of_lt_of_le one_lt_two hn)),
Finset.prod_insert (Finset.notMem_erase 1 _), cyclotomic_one R]
have hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j :=
by
intro j hj
apply Nat.succ_le_of_lt
exact
(Ne.le_iff_lt (Finset.mem_erase.1 hj).1.symm).mp
(Nat.succ_le_of_lt (Nat.pos_of_mem_properDivisors (Finset.mem_erase.1 hj).2))
have hcongr : ∀ j ∈ n.properDivisors.erase 1, (cyclotomic j R).coeff 0 = 1 :=
by
intro j hj
exact hi j (Nat.mem_properDivisors.1 (Finset.mem_erase.1 hj).2).2 (hleq j hj)
have hrw : (∏ x ∈ n.properDivisors.erase 1, (cyclotomic x R).coeff 0) = 1 :=
by
rw [Finset.prod_congr (refl (n.properDivisors.erase 1)) hcongr]
simp only [Finset.prod_const_one]
simp only [hrw, mul_one, zero_sub, coeff_one_zero, coeff_X_zero, coeff_sub]
have heq : (X ^ n - 1 : R[X]).coeff 0 = -(cyclotomic n R).coeff 0 := by
rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ← Nat.cons_self_properDivisors hn.ne_bot,
Finset.prod_cons, mul_coeff_zero, coeff_zero_prod, hprod, mul_neg, mul_one]
have hzero : (X ^ n - 1 : R[X]).coeff 0 = (-1 : R) :=
by
rw [coeff_zero_eq_eval_zero _]
simp only [zero_pow (by positivity : n ≠ 0), eval_X, eval_one, zero_sub, eval_pow, eval_sub]
rw [hzero] at heq
exact neg_inj.mp (Eq.symm heq)
