map_right_cancel — Mathlib

English

If algebraMap R S (c·x) = algebraMap R S (c·y) for some c ∈ M, then algebraMap R S x = algebraMap R S y.

Русский

Если f(cx) = f(cy) для некоторого c ∈ M, то f(x) = f(y).

LaTeX

$$$\\forall x,y\\in R\\,\\forall c\\in M,\\;\\,\\alpha(c x) = \\alpha(c y) \\Rightarrow \\alpha(x) = \\alpha(y)$, where $\\alpha = \\text{algebraMap } R S$$$

Lean4

theorem map_right_cancel {x y} {c : M} (h : algebraMap R S (c * x) = algebraMap R S (c * y)) :
    algebraMap R S x = algebraMap R S y :=
  (toLocalizationMap M S).map_right_cancel h

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