leftInverse_inv_mul_mul_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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