instIsCyclotomicExtensionSingletonNatSetOfNat

English

There is a cyclotomic extension instance for singleton {0} over K, for natural numbers, under CharZero assumptions when appropriate.

Русский

Существуют примеры циклотомических расширений для одиночного множества {0} над K при заданных условиях.

LaTeX

$$$IsCyclotomicExtension\\{0\\} K (CyclotomicField 0 K)$$$

Lean4

instance : IsCyclotomicExtension {0} K (CyclotomicField 0 K)
    where
  exists_isPrimitiveRoot := by aesop
  adjoin_roots
    x :=
    by
    have finrank : Module.finrank K (CyclotomicField 0 K) = 1 :=
      by
      have : Polynomial.IsSplittingField K K (Polynomial.cyclotomic 0 K) := Polynomial.isSplittingField_C 1
      let e : K ≃ₗ[K] (CyclotomicField 0 K) :=
        (Polynomial.IsSplittingField.algEquiv K (Polynomial.cyclotomic 0 K)).toLinearEquiv
      simp [← LinearEquiv.finrank_eq e, finrank_self]
    simp [Subalgebra.bot_eq_top_iff_finrank_eq_one.mpr finrank]

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