mk0_surjective — Mathlib

English

Every class in the class group has a representative coming from a nonzero ideal via mk0.

Русский

Каждому классу в группе классов соответствует представитель, полученный из ненулевого идеала через mk0.

LaTeX

$$$\text{Surjective}(\mathrm{ClassGroup.mk0})$$$

Lean4

theorem mk0_surjective [IsDedekindDomain R] : Function.Surjective (ClassGroup.mk0 : (Ideal R)⁰ → ClassGroup R) :=
  by
  rintro ⟨I⟩
  refine ⟨⟨ClassGroup.integralRep I.1, ClassGroup.integralRep_mem_nonZeroDivisors I.ne_zero⟩, ?_⟩
  rw [ClassGroup.mk0_integralRep, ClassGroup.Quot_mk_eq_mk]

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