adjoin_isCyclotomicExtension — 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 (adjoin A \\{ζ\\})$$$

Lean4

theorem _root_.IsPrimitiveRoot.adjoin_isCyclotomicExtension {ζ : B} {n : ℕ} [NeZero n] (h : IsPrimitiveRoot ζ n) :
    IsCyclotomicExtension { n } A (adjoin A ({ ζ } : Set B)) :=
  { exists_isPrimitiveRoot := fun hi hi' => by
      rw [Set.mem_singleton_iff] at hi
      refine ⟨⟨ζ, subset_adjoin <| Set.mem_singleton ζ⟩, ?_⟩
      rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk, hi]
    adjoin_roots := fun ⟨x, hx⟩ =>
      by
      refine
        adjoin_induction (hx := hx) (fun b hb => ?_) (fun a => ?_) (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
          (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
      · rw [Set.mem_singleton_iff] at hb
        refine subset_adjoin ?_
        simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq, hb]
        rw [← Subalgebra.coe_eq_one, Subalgebra.coe_pow, Subtype.coe_mk]
        exact ⟨NeZero.ne n, ((IsPrimitiveRoot.iff_def ζ n).1 h).1⟩
      · exact Subalgebra.algebraMap_mem _ _
      · exact Subalgebra.add_mem _ hb₁ hb₂
      · exact Subalgebra.mul_mem _ hb₁ hb₂ }

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