English
For a primitive root ζ of order p^k in a cyclotomic extension, the gen of subOneIntegralPowerBasis is ζ − 1 with the appropriate subalgebra membership proof.
Русский
Для примитивного корня ζ порядка p^k в циклотомическом расширении, gen подOneIntegralPowerBasis равен ζ − 1 с доказательством принадлежности подалгебре.
LaTeX
$$$$ h\zeta.subOneIntegralPowerBasis.gen = \langle \zeta - 1, \text{Subalgebra.sub_mem}(\dots) \rangle $$$$
Lean4
/-- The integral `PowerBasis` of `𝓞 K` given by `ζ - 1`, where `K` is a `p ^ k` cyclotomic
extension of `ℚ`. -/
noncomputable def subOneIntegralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
PowerBasis ℤ (𝓞 K) :=
PowerBasis.ofAdjoinEqTop' (RingOfIntegers.isIntegral ⟨ζ - 1, (hζ.isIntegral (NeZero.pos _)).sub isIntegral_one⟩)
(by
refine hζ.integralPowerBasis.adjoin_eq_top_of_gen_mem_adjoin ?_
convert Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)
simp [RingOfIntegers.ext_iff, integralPowerBasis_gen, toInteger])
