finite_quotient_span_sub_one — Mathlib

English

The quotient of the ring of integers by the ideal generated by hζ.toInteger − 1 is finite.

Русский

Квотиент кольца целых по идеалу, порождённому hζ.toInteger − 1, конечен.

LaTeX

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

Lean4

theorem finite_quotient_span_sub_one [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) : Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) :=
  by
  have : NumberField K := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
  refine Ideal.finiteQuotientOfFreeOfNeBot _ (fun h ↦ ?_)
  simp only [Ideal.span_singleton_eq_bot, sub_eq_zero] at h
  exact hζ.ne_one (one_lt_pow₀ hp.1.one_lt (Nat.zero_ne_add_one k).symm) (RingOfIntegers.ext_iff.1 h)

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