English
If a and b commute in a monoid with zero, then inverse(ab) = inverse(b) · inverse(a); the identity also holds when the product is not a unit, by the zero-case convention.
Русский
Если a и b commute в моноиде с нулём, то inverse(ab) = inverse(b) · inverse(a); в общем случае с не-единичный случай учитывается через определение inverse.
LaTeX
$$$\text{inverse}(a b) = \text{inverse}(b) \cdot \text{inverse}(a)$ при $\text{Commute}(a,b)$$$
Lean4
theorem mul_inverse_rev' {a b : M₀} (h : Commute a b) : inverse (a * b) = inverse b * inverse a :=
by
by_cases hab : IsUnit (a * b)
· obtain ⟨⟨a, rfl⟩, b, rfl⟩ := h.isUnit_mul_iff.mp hab
rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]
obtain ha | hb := not_and_or.mp (mt h.isUnit_mul_iff.mpr hab)
· rw [inverse_non_unit _ hab, inverse_non_unit _ ha, mul_zero]
· rw [inverse_non_unit _ hab, inverse_non_unit _ hb, zero_mul]
