integralPowerBasis'_gen — Mathlib

English

For a p-th cyclotomic extension with p prime, the gen of integralPowerBasis' equals the integer root hζ.toInteger.

Русский

Для p-й циклотомической перестройки с простым p, элемент gen интегральной мощности базы равен hζ.toInteger.

LaTeX

$$$$ h\zeta.integralPowerBasis'.gen = h\zeta.toInteger $$$$

Lean4

@[simp]
theorem integralPowerBasis'_gen [hcycl : IsCyclotomicExtension { p } ℚ K] (hζ : IsPrimitiveRoot ζ p) :
    hζ.integralPowerBasis'.gen = hζ.toInteger :=
  integralPowerBasis_gen (hcycl := by rwa [pow_one]) (by rwa [pow_one])

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