English
Two elements a,b of integerSet K map to the same associate class iff there exists a torsion element ζ with ζ•a = b.
Русский
Два элемента a,b из integerSet K имеют одинаковый ассоциатный класс тогда и только тогда, когда существует торовая элемент ζ, такой что ζ·a = b.
LaTeX
$$$\\operatorname{integerSetToAssociates}\\;K\\;a = \\operatorname{integerSetToAssociates}\\;K\\;b \\iff \\exists \\zeta:\\operatorname{torsion}K, \\; \\zeta\\cdot a = b.$$$
Lean4
theorem integerSetToAssociates_eq_iff (a b : integerSet K) :
integerSetToAssociates K a = integerSetToAssociates K b ↔ ∃ ζ : torsion K, ζ • a = b :=
by
simp_rw [integerSetToAssociates_apply, Associates.quotient_mk_eq_mk, Associates.mk_eq_mk_iff_associated, Associated,
mul_comm, Subtype.ext_iff, RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff, Submonoid.coe_mul,
map_mul, mixedEmbedding_preimageOfMemIntegerSet, integerSetTorsionSMul_smul_coe]
refine
⟨fun ⟨u, h⟩ ↦ ⟨⟨unitsNonZeroDivisorsEquiv u, ?_⟩, by simpa using h⟩, fun ⟨⟨u, _⟩, h⟩ ↦
⟨unitsNonZeroDivisorsEquiv.symm u, by simpa using h⟩⟩
exact (unit_smul_mem_iff_mem_torsion a.prop.1 _).mp (by simpa [h] using b.prop.1)
