leftInverse_mul_right_inv_mul — Mathlib

English

For any c ∈ G, multiplication on the left by c followed by multiplication by c^{-1} on the left is the identity, i.e., c * (c^{-1} * x) = x.

Русский

Для любого c ∈ G произведение слева на c и последующее умножение на c^{-1} слева дают тождество: c · (c^{-1} · x) = x.

LaTeX

$$$\forall x \in G,\ c \cdot (c^{-1} \cdot x) = x.$$

Lean4

@[to_additive]
theorem leftInverse_mul_right_inv_mul (c : G) : Function.LeftInverse (fun x ↦ c * x) fun x ↦ c⁻¹ * x := fun x ↦
  mul_inv_cancel_left c x

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