English
The value of mk on a unit fractional ideal is the same as the corresponding image under the principal-ideal quotient construction.
Русский
Значение mk на единичном дробном идеале совпадает с изображением через соответствующее отображение по принципиальному идеалу в фактор-группе.
LaTeX
$$$\mathrm{mk}(I) = (\mathrm{QuotientGroup.mk'}(\mathrm{toPrincipalIdeal}(R,\mathrm{FractionRing}(R)).\mathrm{range}))\big(\mathrm{Units.map}(\mathrm{FractionalIdeal.canonicalEquiv}(R^{0},K,\mathrm{FractionRing}(R)))(I)\big).$$$
Lean4
theorem mk_def (I : (FractionalIdeal R⁰ K)ˣ) :
ClassGroup.mk I =
(QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
(Units.map (FractionalIdeal.canonicalEquiv R⁰ K (FractionRing R)) I) :=
rfl
