subOneIntegralPowerBasis_gen — Mathlib

English

In a cyclotomic extension, the subOneIntegralPowerBasis generator equals the ζ − 1 element with the associated membership proof.

Русский

В циклотомическом расширении генератор subOneIntegralPowerBasis равен элементу ζ − 1 с доказательством принадлежности.

LaTeX

$$$$ h\zeta.subOneIntegralPowerBasis.gen = \langle \zeta - 1, \text{Subalgebra.sub_mem}(\dots) \rangle $$$$

Lean4

@[simp]
theorem subOneIntegralPowerBasis_gen [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
    hζ.subOneIntegralPowerBasis.gen =
      ⟨ζ - 1, Subalgebra.sub_mem _ (hζ.isIntegral (NeZero.pos _)) (Subalgebra.one_mem _)⟩ :=
  by simp [subOneIntegralPowerBasis]

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