mk'_eq_of_eq' — Mathlib

English

For any a ∈ R and b,c ∈ M, mk' S (a c) b = mk' S a (b) cancels c on the left.

Русский

Для любых a ∈ R и b,c ∈ M выполняется mk' S (a c) b = mk' S a b, то есть левый множитель c отменяется.

LaTeX

$$$mk' S (a \\cdot c) \\; b = mk' S a b \\\\ (c \\in M)$$$

Lean4

theorem mk'_eq_of_eq' {a₁ b₁ : R} {a₂ b₂ : M} (H : b₁ * ↑a₂ = a₁ * ↑b₂) : mk' S a₁ a₂ = mk' S b₁ b₂ :=
  (toLocalizationMap M S).mk'_eq_of_eq' H

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