finite_quotient_toInteger_sub_one

English

For a number field K with ζ a primitive root of unity in a cyclotomic extension, the quotient 𝓞_K / (ζ − 1) is finite.

Русский

Для числового поля K, в циклотомическом расширении ζ — примитивная корневая единица; частное 𝓞_K / (ζ − 1) конечно.

LaTeX

$$$$ \text{Finite} \left( \mathcal{O}_K \;/\; (\zeta - 1) \right) $$$$

Lean4

/-- `𝓞 K ⧸ Ideal.span {ζ - 1}` is finite. -/
theorem finite_quotient_toInteger_sub_one [NumberField K] {k : ℕ} (hk : 1 < k) (hζ : IsPrimitiveRoot ζ k) :
    haveI : NeZero k := NeZero.of_gt hk
    Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) :=
  by
  refine Ideal.finiteQuotientOfFreeOfNeBot _ (fun h ↦ ?_)
  simp only [Ideal.span_singleton_eq_bot, sub_eq_zero] at h
  exact hζ.ne_one hk (RingOfIntegers.ext_iff.1 h)

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