subOneIntegralPowerBasis'_gen — Mathlib

English

For a p-th cyclotomic extension with p prime, the gen of subOneIntegralPowerBasis' equals hζ.toInteger − 1.

Русский

Для p-й циклотомической расширения с простым p, gen subOneIntegralPowerBasis' равен hζ.toInteger − 1.

LaTeX

$$$$ h\zeta.subOneIntegralPowerBasis'.gen = h\zeta.toInteger - 1 $$$$

Lean4

@[simp, nolint unusedHavesSuffices]
theorem subOneIntegralPowerBasis'_gen [IsCyclotomicExtension { p } ℚ K] (hζ : IsPrimitiveRoot ζ p) :
    hζ.subOneIntegralPowerBasis'.gen = hζ.toInteger - 1 :=
  -- The `unusedHavesSuffices` linter incorrectly thinks this `have` is unnecessary.

  have : IsCyclotomicExtension {p ^ 1} ℚ K := by rwa [pow_one]
  subOneIntegralPowerBasis_gen (by rwa [pow_one])

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