mul_inverse_rev — Mathlib

English

In a commutative monoid with zero, the inverse of a product equals the product of inverses in reverse order: inverse(ab) = inverse(b) · inverse(a).

Русский

В коммутативном моноиде с нулём обратная произведения равна произведению обратных в обратном порядке: inverse(ab) = inverse(b) · inverse(a).

LaTeX

$$$\text{inverse}(a \cdot b) = \text{inverse}(b) \cdot \text{inverse}(a)$$$

Lean4

theorem mul_inverse_rev {M₀} [CommMonoidWithZero M₀] (a b : M₀) : Ring.inverse (a * b) = inverse b * inverse a :=
  mul_inverse_rev' (Commute.all _ _)

Похожие утверждения