English
For division monoids, s * t = 1 holds iff there exist a,b with s = {a}, t = {b}, and a*b = 1.
Русский
В разделе моноидов деления, s * t = 1 эквивалентно существованию a,b таких, что s = {a}, t = {b} и a*b = 1.
LaTeX
$$$s * t = 1 \iff \exists a \exists b, s = \{a\} \land t = \{b\} \land a \cdot b = 1$$$
Lean4
@[to_additive]
protected theorem mul_eq_one_iff : s * t = 1 ↔ ∃ a b, s = { a } ∧ t = { b } ∧ a * b = 1 :=
by
refine ⟨fun h => ?_, ?_⟩
· have hst : (s * t).Nonempty := h.symm.subst one_nonempty
obtain ⟨a, ha⟩ := hst.of_image2_left
obtain ⟨b, hb⟩ := hst.of_image2_right
have H : ∀ {a b}, a ∈ s → b ∈ t → a * b = (1 : α) := fun {a b} ha hb => h.subset <| mem_image2_of_mem ha hb
refine ⟨a, b, ?_, ?_, H ha hb⟩ <;> refine eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => ?_⟩
· exact (eq_inv_of_mul_eq_one_left <| H hx hb).trans (inv_eq_of_mul_eq_one_left <| H ha hb)
· exact (eq_inv_of_mul_eq_one_right <| H ha hx).trans (inv_eq_of_mul_eq_one_right <| H ha hb)
· rintro ⟨b, c, rfl, rfl, h⟩
rw [singleton_mul_singleton, h, singleton_one]
