inv_mul_mul_self — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Multiplying `a⁻¹` by `a` twice results in `a` (whether or not `a`
is zero). -/
@[simp]
theorem inv_mul_mul_self (a : G₀) : a⁻¹ * a * a = a :=
  by
  by_cases h : a = 0
  · rw [h, inv_zero, mul_zero]
  · rw [inv_mul_cancel₀ h, one_mul]

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