subOneIntegralPowerBasis' — Mathlib

English

Equality expressing subOneIntegralPowerBasis.gen in terms of ζ − 1 inside the integral power basis framework.

Русский

Равенство, выражающее subOneIntegralPowerBasis.gen через ζ − 1 в рамках интегральной базы мощности.

LaTeX

$$$$ h\zeta.subOneIntegralPowerBasis.gen = \langle \zeta - 1, \dots \rangle $$$$

Lean4

/-- The integral `PowerBasis` of `𝓞 K` given by `ζ - 1`, where `K` is a `p`-th cyclotomic
extension of `ℚ`. -/
noncomputable def subOneIntegralPowerBasis' [IsCyclotomicExtension { p } ℚ K] (hζ : IsPrimitiveRoot ζ p) :
    PowerBasis ℤ (𝓞 K) :=
  have : IsCyclotomicExtension {p ^ 1} ℚ K := by rwa [pow_one]
  subOneIntegralPowerBasis (p := p) (k := 1) (ζ := ζ) (by rwa [pow_one])

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