integralPowerBasis_dim — Mathlib

English

For primitive p-th roots and p^k-cyclotomic extensions with p prime, the dimension of the integral power basis is φ(p^k).

Русский

Для примитивных p-й корней и p^k-циклотомических расширений с простым p размерность интегрального мощности базиса равна φ(p^k).

LaTeX

$$$$ \dim_{K} (\text{integralPowerBasis}) = \varphi(p^k) $$$$

Lean4

@[simp]
theorem integralPowerBasis_dim [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
    hζ.integralPowerBasis.dim = φ (p ^ k) := by
  simp [integralPowerBasis, ← cyclotomic_eq_minpoly hζ (NeZero.pos _), natDegree_cyclotomic]

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