English
For a prime p and a natural n, the cyclotomic polynomial cyclotomic(p^(n+1)) composed with X+1 is Eisenstein at the ideal generated by p in Z.
Русский
Для простого p и натурального n полином Циклотомический(p^(n+1)), композиция с X+1 является Эйзенштейновым относительно идеала, порождённого p в Z.
LaTeX
$$$\\forall p\\text{ prime}, \\; (cyclotomic(p^{n+1}, \\mathbb Z) \\circ (X+1)).IsEisensteinAt (\\mathcal P)$ with \\mathcal P = \\langle p \\rangle$$$
Lean4
theorem cyclotomic_comp_X_add_one_isEisensteinAt [hp : Fact p.Prime] :
((cyclotomic p ℤ).comp (X + 1)).IsEisensteinAt 𝓟 :=
by
refine
Monic.isEisensteinAt_of_mem_of_notMem ?_
(Ideal.IsPrime.ne_top <|
(Ideal.span_singleton_prime (mod_cast hp.out.ne_zero)).2 <| Nat.prime_iff_prime_int.1 hp.out)
(fun {i hi} => ?_) ?_
· rw [show (X + 1 : ℤ[X]) = X + C 1 by simp]
refine (cyclotomic.monic p ℤ).comp (monic_X_add_C 1) fun h => ?_
rw [natDegree_X_add_C] at h
exact zero_ne_one h.symm
· rw [cyclotomic_prime, geom_sum_X_comp_X_add_one_eq_sum, ← lcoeff_apply, map_sum]
conv =>
congr
congr
next => skip
congr
next => skip
ext
rw [lcoeff_apply, ← C_eq_natCast, C_mul_X_pow_eq_monomial, coeff_monomial]
rw [natDegree_comp, show (X + 1 : ℤ[X]) = X + C 1 by simp, natDegree_X_add_C, mul_one, natDegree_cyclotomic,
Nat.totient_prime hp.out] at hi
simp only [hi.trans_le (Nat.sub_le _ _), sum_ite_eq', mem_range, if_true, Ideal.submodule_span_eq,
Ideal.mem_span_singleton, Int.natCast_dvd_natCast]
exact hp.out.dvd_choose_self i.succ_ne_zero (lt_tsub_iff_right.1 hi)
· rw [coeff_zero_eq_eval_zero, eval_comp, cyclotomic_prime, eval_add, eval_X, eval_one, zero_add, eval_geom_sum,
one_geom_sum, Ideal.submodule_span_eq, Ideal.span_singleton_pow, Ideal.mem_span_singleton]
intro h
obtain ⟨k, hk⟩ := Int.natCast_dvd_natCast.1 h
rw [mul_assoc, mul_comm 1, mul_one] at hk
nth_rw 1 [← Nat.mul_one p] at hk
rw [mul_right_inj' hp.out.ne_zero] at hk
exact Nat.Prime.not_dvd_one hp.out (Dvd.intro k hk.symm)
