English
In an algebraic setting with a primitive root ζ of order n and IsCyclotomicExtension {n} K A, the minimal polynomial of ζ − 1 over K equals the cyclotomic polynomial of n evaluated at X + 1.
Русский
В алгебраической системе с примитивным ζ порядка n и IsCyclotomicExtension{n} K A минимальный многочлен ζ − 1 над K равен циклотомическому многочлену n в X + 1.
LaTeX
$$$\minpoly_K(\zeta - 1) = (\operatorname{cyclotomic}_n K) \circ (X + 1)$$$
Lean4
/-- If `Irreducible (cyclotomic n K)` (in particular for `K = ℚ`), then the norm of
`ζ - 1` is `eval 1 (cyclotomic n ℤ)`. -/
theorem sub_one_norm_eq_eval_cyclotomic [IsCyclotomicExtension { n } K L] (h : 2 < n)
(hirr : Irreducible (cyclotomic n K)) : norm K (ζ - 1) = ↑(eval 1 (cyclotomic n ℤ)) :=
by
haveI := IsCyclotomicExtension.neZero' n K L
let E := AlgebraicClosure L
obtain ⟨z, hz⟩ := IsAlgClosed.exists_root _ (degree_cyclotomic_pos n E (NeZero.pos _)).ne.symm
apply (algebraMap K E).injective
letI := IsCyclotomicExtension.finiteDimensional { n } K L
letI := IsCyclotomicExtension.isGalois { n } K L
rw [norm_eq_prod_embeddings]
conv_lhs =>
congr
rfl
ext
rw [← neg_sub, map_neg, map_sub, map_one, neg_eq_neg_one_mul]
rw [prod_mul_distrib, prod_const, Finset.card_univ, AlgHom.card, IsCyclotomicExtension.finrank L hirr,
(totient_even h).neg_one_pow, one_mul]
have Hprod : (Finset.univ.prod fun σ : L →ₐ[K] E => 1 - σ ζ) = eval 1 (cyclotomic' n E) :=
by
rw [cyclotomic', eval_prod, ← @Finset.prod_attach E E, ← univ_eq_attach]
refine Fintype.prod_equiv (hζ.embeddingsEquivPrimitiveRoots E hirr) _ _ fun σ => ?_
simp
have : NeZero (n : E) := NeZero.of_faithfulSMul K _ n
rw [Hprod, cyclotomic', ← cyclotomic_eq_prod_X_sub_primitiveRoots (isRoot_cyclotomic_iff.1 hz), ← map_cyclotomic_int,
_root_.map_intCast, ← Int.cast_one, eval_intCast_map, eq_intCast, Int.cast_id]
