English
Let α be a MonoidWithZero in which every nonzero a has a left inverse; then every nonzero a has a right inverse.
Русский
Пусть α — моноид с нулём, в котором каждый ненулевой элемент имеет левый обратный; тогда у каждого ненулевого элемента есть правый обратный.
LaTeX
$$$$ (\forall a \neq 0, \exists b, b \cdot a = 1) \implies (\forall a \neq 0, \exists b, a \cdot b = 1) $$$$
Lean4
theorem exists_right_inv_of_exists_left_inv {α} [MonoidWithZero α] (h : ∀ a : α, a ≠ 0 → ∃ b : α, b * a = 1) {a : α}
(ha : a ≠ 0) : ∃ b : α, a * b = 1 :=
by
obtain _ | _ := subsingleton_or_nontrivial α
· exact ⟨a, Subsingleton.elim _ _⟩
obtain ⟨b, hb⟩ := h a ha
obtain ⟨c, hc⟩ := h b (left_ne_zero_of_mul <| hb.trans_ne one_ne_zero)
refine ⟨b, ?_⟩
conv_lhs => rw [← one_mul (a * b), ← hc, mul_assoc, ← mul_assoc b, hb, one_mul, hc]
