power_basis_int'_dim — Mathlib

English

In a p-th cyclotomic extension of ℚ with p prime, the dimension of integralPowerBasis' equals φ(p).

Русский

В p-й циклотомической расширении над ℚ с простым p размерность integralPowerBasis' равна φ(p).

LaTeX

$$$$ \dim( h\zeta.integralPowerBasis' ) = \varphi(p) $$$$

Lean4

@[simp]
theorem power_basis_int'_dim [hcycl : IsCyclotomicExtension { p } ℚ K] (hζ : IsPrimitiveRoot ζ p) :
    hζ.integralPowerBasis'.dim = φ p := by
  rw [integralPowerBasis', integralPowerBasis_dim (hcycl := by rwa [pow_one]) (by rwa [pow_one]), pow_one]

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