English
mkMMem is defined such that it provides a surjective map onto the class group, pulling back through mk0.
Русский
mkMMem задаёт сюръективное отображение на класс-группу через mk0.
LaTeX
$$mkMMem : (ClassGroup S) → ClassGroup S is surjective$$
Lean4
/-- `ClassGroup.mkMMem` is a specialization of `ClassGroup.mk0` to (the finite set of)
ideals that contain `M := ∏ m ∈ finsetApprox L f abs, m`.
By showing this function is surjective, we prove that the class group is finite. -/
noncomputable def mkMMem [IsDedekindDomain S]
(J : { J : Ideal S // algebraMap _ _ (∏ m ∈ finsetApprox bS adm, m) ∈ J }) : ClassGroup S :=
ClassGroup.mk0 ⟨J.1, mem_nonZeroDivisors_iff_ne_zero.mpr (ne_bot_of_prod_finsetApprox_mem bS adm J.1 J.2)⟩
