English
Two unit fractional ideals I and J determine the same class iff there exists a nonzero element x in the fraction field such that I·(x) = J.
Русский
Два единичных дробных идеала I и J определяют один и тот же класс тогда и только тогда, когда существует ненулевой элемент x в дробной зоне, такой что I·(x) = J.
LaTeX
$$$\mathrm{ClassGroup.mk}(I) = \mathrm{ClassGroup.mk}(J) \iff \exists x \in (\mathrm{FractionRing}(R))^{\times},\; I \cdot \text{toPrincipalIdeal}(R,\mathrm{FractionRing}(R))(x) = J.$$$
Lean4
theorem mk_eq_mk {I J : (FractionalIdeal R⁰ <| FractionRing R)ˣ} :
ClassGroup.mk I = ClassGroup.mk J ↔ ∃ x : (FractionRing R)ˣ, I * toPrincipalIdeal R (FractionRing R) x = J :=
by
rw [mk_def, mk_def, QuotientGroup.mk'_eq_mk']
simp [RingEquiv.coe_monoidHom_refl, MonoidHom.mem_range, -toPrincipalIdeal_eq_iff]
