map_left_cancel — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall x,y\\in R\\,\\forall c\\in M,\\;\\alpha(x c) = \\alpha(y c) \\Rightarrow \\alpha(x) = \\alpha(y)$$$

Lean4

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

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