intermediateField_adjoin_isCyclotomicExtension

English

If h provides primitive roots for all n in S, then IsCyclotomicExtension S K (IntermediateField.adjoin K {b ∈ L | ∃ n ∈ S, n ≠ 0 ∧ b^n = 1}).

Русский

Если для всех n ∈ S существуют примитивные корни, то IsCyclotomicExtension S K (IntermediateField.adjoin K {b ∈ L | ∃ n ∈ S, n ≠ 0 ∧ b^n = 1}).

LaTeX

$$$(\\forall n \\in S) \\ (n ≠ 0) \\Rightarrow IsCyclotomicExtension S K (IntermediateField.adjoin K \\{b : L \\mid \\exists n \\in S, n \\neq 0 ∧ b^n = 1\\})$$$

Lean4

theorem _root_.IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension [Algebra.IsIntegral K L] {n : ℕ}
    [NeZero n] {ζ : L} (hζ : IsPrimitiveRoot ζ n) : IsCyclotomicExtension { n } K (IntermediateField.adjoin K { ζ }) :=
  by
  change IsCyclotomicExtension { n } K (IntermediateField.adjoin K { ζ }).toSubalgebra
  rw [IntermediateField.adjoin_simple_toSubalgebra_of_integral (IsIntegral.isIntegral ζ)]
  exact hζ.adjoin_isCyclotomicExtension K

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