mul_self_mul_inv — Mathlib

English

For any element a in a group with zero, the product a · a · a^{-1} equals a.

Русский

Для любого элемента a в группе с нулём произведение a · a · a^{-1} равно a.

LaTeX

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

Lean4

/-- Multiplying `a` by itself and then by its inverse results in `a`
(whether or not `a` is zero). -/
@[simp]
theorem mul_self_mul_inv (a : G₀) : a * a * a⁻¹ = a :=
  by
  by_cases h : a = 0
  · rw [h, inv_zero, mul_zero]
  · rw [mul_assoc, mul_inv_cancel₀ h, mul_one]

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