English
If ζ is a primitive n-th root with IsCyclotomicExtension {n} K A and the irreducibility of cyclotomic n K holds, then the minimal polynomial of ζ − 1 equals the cyclotomic polynomial composed with X + 1 (as in 149232).
Русский
Если ζ — примитивный корень порядка n, и IsCyclotomicExtension{n} K A, а циклотомический n K ирреducible, то minpoly(ζ − 1) = cyclotomic_n K ∘ (X + 1).
LaTeX
$$$\minpoly_K(\zeta - 1) = (\operatorname{cyclotomic}_n K) \circ (X + 1)$$$
Lean4
theorem minpoly_sub_one_eq_cyclotomic_comp [Algebra K A] [IsDomain A] {ζ : A} [IsCyclotomicExtension { n } K A]
(hζ : IsPrimitiveRoot ζ n) (h : Irreducible (Polynomial.cyclotomic n K)) :
minpoly K (ζ - 1) = (cyclotomic n K).comp (X + 1) :=
by
haveI := IsCyclotomicExtension.neZero' n K A
rw [show ζ - 1 = ζ + algebraMap K A (-1) by simp [sub_eq_add_neg], minpoly.add_algebraMap ζ,
hζ.minpoly_eq_cyclotomic_of_irreducible h]
simp
