div_mul_cancel_left — Mathlib

English

Let G be a commutative group. For all a, b ∈ G, a * (b * a^{-1}) = b.

Русский

Пусть G — коммутативная группа. Для любых a, b ∈ G выполняется a · (b · a^{-1}) = b.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem div_mul_cancel_left (a b : G) : a / (a * b) = b⁻¹ := by
  rw [← inv_div, mul_div_cancel_left]
    -- This lemma is in the `simp` set under the name `mul_inv_cancel_comm_assoc`,
    -- along with the additive version `add_neg_cancel_comm_assoc`,
    -- defined in `Algebra.Group.Commute`

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