mul_inv_mul_cancel — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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