leftInverse_div_mul_left — Mathlib

English

For any c ∈ G, the map x ↦ x / c has a left inverse given by x ↦ x * c, i.e., (x * c) / c = x.

Русский

Для любого c ∈ G отображение x ↦ x / c имеет левый обратный, равный x ↦ x * c, то есть (x c) / c = x.

LaTeX

$$$\forall x \in G,\ (x \cdot c)/c = x.$$

Lean4

@[to_additive]
theorem leftInverse_div_mul_left (c : G) : Function.LeftInverse (fun x ↦ x / c) fun x ↦ x * c := fun x ↦
  mul_div_cancel_right x c

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