English
In a division monoid, f * g = 1 if and only if there exist a,b with f = pure a, g = pure b and a * b = 1.
Русский
В дивизионном моноиде, f * g = 1 тогда и только тогда, когда существуют a,b такие что f = pure(a), g = pure(b) и a*b = 1.
LaTeX
$$$f * g = 1 \iff \exists a,b,\ f = \text{pure}(a) \land g = \text{pure}(b) \land a * b = 1.$$$
Lean4
@[to_additive]
protected theorem mul_eq_one_iff : f * g = 1 ↔ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1 :=
by
refine ⟨fun hfg => ?_, ?_⟩
· obtain ⟨t₁, h₁, t₂, h₂, h⟩ : (1 : Set α) ∈ f * g := hfg.symm ▸ one_mem_one
have hfg : (f * g).NeBot := hfg.symm.subst one_neBot
rw [(hfg.nonempty_of_mem <| mul_mem_mul h₁ h₂).subset_one_iff, Set.mul_eq_one_iff] at h
obtain ⟨a, b, rfl, rfl, h⟩ := h
refine ⟨a, b, ?_, ?_, h⟩
· rwa [← hfg.of_mul_left.le_pure_iff, le_pure_iff]
· rwa [← hfg.of_mul_right.le_pure_iff, le_pure_iff]
· rintro ⟨a, b, rfl, rfl, h⟩
rw [pure_mul_pure, h, pure_one]
