one_div_mul_one_div_rev — Mathlib

English

In any division monoid, the product of the inverses equals the inverse of the reversed product: a^{-1} b^{-1} = (b a)^{-1}. Equivalently, 1/a · 1/b = 1/(b a).

Русский

В любом дивизионном моноиде произведение обратных элементов равно обратному произведению в обратном порядке: a^{-1} b^{-1} = (b a)^{-1}. Эквивалентно 1/a · 1/b = 1/(b a).

LaTeX

$$$a^{-1} \\cdot b^{-1} = (b a)^{-1}$$$

Lean4

@[to_additive]
theorem one_div_mul_one_div_rev : 1 / a * (1 / b) = 1 / (b * a) := by simp

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