isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot

English

If S is finite and IsCyclotomicExtension S K L with K a number field, then L is a number field.

Русский

Если S конечное и IsCyclotomicExtension S K L с K — число поле, то L — число поле.

LaTeX

$$$[h : NumberField K] [Finite S] [IsCyclotomicExtension S K L] \\Rightarrow NumberField L$$$

Lean4

theorem _root_.IntermediateField.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot
    (h : ∀ n ∈ S, n ≠ 0 → ∃ r : L, IsPrimitiveRoot r n) :
    IsCyclotomicExtension S K (IntermediateField.adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) :=
  by
  have key : ∀ b ∈ {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}, IsAlgebraic K b :=
    by
    rintro b ⟨n, hn, h1, h2⟩
    exact ⟨X ^ n - 1, (monic_X_pow_sub_C (1 : K) h1).ne_zero, by simp [h2]⟩
  change IsCyclotomicExtension S K (IntermediateField.toSubalgebra _)
  rw [congr(IsCyclotomicExtension S K $(IntermediateField.adjoin_algebraic_toSubalgebra key))]
  exact Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot S K L h

Похожие утверждения