mul_inv — Mathlib

English

Let G be a division monoid and take a, b ∈ G that commute. Then the inverse of their product equals the product of their inverses in the same order: (a b)^{-1} = a^{-1} b^{-1}.

Русский

Пусть G — делимый моноид и элементы a, b ∈ G commute. Тогда обратный к произведению равен произведению обратных в том же порядке: (ab)^{-1} = a^{-1} b^{-1}.

LaTeX

$$$Commute(a,b) \Rightarrow (ab)^{-1} = a^{-1} b^{-1}$$$

Lean4

@[to_additive]
protected theorem mul_inv (hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by rw [hab.eq, mul_inv_rev]

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