English
Let n be a natural number and let L be a cyclotomic extension of K by n over ℚ; if Φ_n is irreducible over K, then the finite rank of L over K equals φ(n).
Русский
Пусть n — натуральное число, и L — циклотомическое расширение базового поля K по отношению к n над ℚ; если многочёт Φ_n ирреducибелен над K, то размерность L над K равна φ(n).
LaTeX
$$$$ \mathrm{finrank}_K L = \varphi(n) $$$$
Lean4
/-- If `Irreducible (cyclotomic n K)` (in particular for `K = ℚ`), then the `finrank` of a
cyclotomic extension is `n.totient`. -/
theorem finrank (hirr : Irreducible (cyclotomic n K)) : finrank K L = n.totient :=
by
haveI := IsCyclotomicExtension.neZero' n K L
rw [((zeta_spec n K L).powerBasis K).finrank, IsPrimitiveRoot.powerBasis_dim, ←
(zeta_spec n K L).minpoly_eq_cyclotomic_of_irreducible hirr, natDegree_cyclotomic]
