English
There is a natural monoid homomorphism that assigns to every nonzero fractional ideal its class in the class group of R.
Русский
Существует естественный моноид-гомоморф, отображающий любой ненулевой дробный идеал в соответствующий класс в группе классов кольца R.
LaTeX
$$$\text{There exists a monoid hom } mk:\;\mathrm{Units}(\mathrm{FractionalIdeal}(\mathrm{nonZeroDivisors}\,R\,K)) \to \mathrm{ClassGroup}(R).$$$
Lean4
/-- Send a nonzero fractional ideal to the corresponding class in the class group. -/
noncomputable def mk : (FractionalIdeal R⁰ K)ˣ →* ClassGroup R :=
(QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range).comp
(Units.map (FractionalIdeal.canonicalEquiv R⁰ K (FractionRing R)))
