finite_quotient_span_sub_one' — Mathlib

English

In the case p is prime, the quotient by span{hζ.toInteger − 1} is finite.

Русский

Когда p простое, фактор-кольцо по порожденному span{hζ.toInteger − 1} конечное.

LaTeX

$$Finite\\HasQuotient\\\$\\mathcal{O}_K / \\langle h\\zeta^{\\mathrm{toInteger}} - 1 \\rangle\\\$$$

Lean4

theorem finite_quotient_span_sub_one' [hcycl : IsCyclotomicExtension { p } ℚ K] (hζ : IsPrimitiveRoot ζ p) :
    Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) :=
  by
  have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl
  replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ
  exact hζ.finite_quotient_span_sub_one

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