adjoinEquivRingOfIntegers' — Mathlib

English

In a p-th cyclotomic extension over ℚ with p prime, the dimension of the integral power basis equals φ(p).

Русский

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

LaTeX

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

Lean4

/-- The algebra isomorphism `adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K)`, where `ζ` is a primitive `p`-th root of
unity and `K` is a `p`-th cyclotomic extension of `ℚ`. -/
@[simps!]
noncomputable def _root_.IsPrimitiveRoot.adjoinEquivRingOfIntegers' [hcycl : IsCyclotomicExtension { p } ℚ K]
    (hζ : IsPrimitiveRoot ζ p) : adjoin ℤ ({ ζ } : Set K) ≃ₐ[ℤ] 𝓞 K :=
  have : IsCyclotomicExtension {p ^ 1} ℚ K := by convert hcycl; rw [pow_one]
  adjoinEquivRingOfIntegers (p := p) (k := 1) (ζ := ζ) (by rwa [pow_one])

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