adjoin_primitive_root_eq_top — Mathlib

English

If ζ is a primitive root of order n, then IsCyclotomicExtension {n} A (adjoin A {ζ}).

Русский

Если ζ — примитивный корень порядка n, то IsCyclotomicExtension {n} A (adjoin A {ζ}).

LaTeX

$$$IsPrimitiveRoot(ζ,n) \\Rightarrow IsCyclotomicExtension\\{n\\} A (\\text{adjoin } A\\{ζ\\})$$$

Lean4

theorem adjoin_primitive_root_eq_top {n : ℕ} [NeZero n] [IsDomain B] [h : IsCyclotomicExtension { n } A B] {ζ : B}
    (hζ : IsPrimitiveRoot ζ n) : adjoin A ({ ζ } : Set B) = ⊤ := by
  classical
  rw [← adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic hζ]
  rw [adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ]
  exact ((iff_adjoin_eq_top { n } A B).mp h).2

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