English
Two nonzero ideals I,J satisfy mk0 I = mk0 J iff there exist nonzero x,y in R with span{x}I = span{y}J in the fraction ring.
Русский
Два не нулевых идеала I,J удовлетворяют mk0 I = mk0 J тогда и только тогда, существует ненулевые x,y в R такие, что span{x}I = span{y}J в дробной зоне.
LaTeX
$$$\mathrm{mk0\_eq\_mk0\_iff}(I,J) \iff \exists x,y\in R, x\neq 0 \land y\neq 0 \land \mathrm{Ideal.span}\{x\} \cdot I = \mathrm{Ideal.span}\{y\} \cdot J.$$$
Lean4
theorem mk0_eq_mk0_iff_exists_fraction_ring [IsDedekindDomain R] {I J : (Ideal R)⁰} :
ClassGroup.mk0 I = ClassGroup.mk0 J ↔ ∃ (x : _) (_ : x ≠ (0 : K)), spanSingleton R⁰ x * I = J :=
by
refine (ClassGroup.equiv K).injective.eq_iff.symm.trans ?_
simp only [ClassGroup.equiv_mk0, QuotientGroup.mk'_eq_mk', mem_principal_ideals_iff, Units.ext_iff, Units.val_mul,
FractionalIdeal.coe_mk0, exists_prop]
constructor
· rintro ⟨X, ⟨x, hX⟩, hx⟩
refine ⟨x, ?_, ?_⟩
· rintro rfl; simp [X.ne_zero.symm] at hX
simpa only [hX, mul_comm] using hx
· rintro ⟨x, hx, eq_J⟩
refine ⟨Units.mk0 _ (spanSingleton_ne_zero_iff.mpr hx), ⟨x, rfl⟩, ?_⟩
simpa only [mul_comm] using eq_J
