English
UniqueMul A B a0 b0 is equivalent to the existence of a unique ab ∈ A×ˢB with ab.1*ab.2 = a0*b0.
Русский
UniqueMul A B a0 b0 эквивалентно существованию единственного элемента ab ∈ A×ˢB с ab.1·ab.2 = a0·b0.
LaTeX
$$$\\mathrm{UniqueMul}\\,A\\,B\\,a_0\\,b_0 \\iff \\exists!\\; ab\\in A\\times^s B \\;\\wedge\\; ab.1*ab.2=a_0*b_0$$$
Lean4
@[to_additive]
theorem iff_existsUnique (aA : a0 ∈ A) (bB : b0 ∈ B) :
UniqueMul A B a0 b0 ↔ ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0 :=
⟨fun _ ↦ ⟨(a0, b0), ⟨Finset.mk_mem_product aA bB, rfl⟩, by simpa⟩, fun h ↦
h.elim
(by
rintro ⟨x1, x2⟩ _ J x y hx hy l
rcases Prod.mk_inj.mp (J (a0, b0) ⟨Finset.mk_mem_product aA bB, rfl⟩) with ⟨rfl, rfl⟩
exact Prod.mk_inj.mp (J (x, y) ⟨Finset.mk_mem_product hx hy, l⟩))⟩
