smul_right_inj — Mathlib

English

For NoZeroSMulDivisors R M, and any c ≠ 0, the equality c•x = c•y is equivalent to x = y for all x,y ∈ M.

Русский

Для NoZeroSMulDivisors R M и любого c ≠ 0 верно: c • x = c • y тогда и только тогда, когда x = y.

LaTeX

$$∀ x y ∈ M, c ∈ R, c ≠ 0 → (c • x = c • y ↔ x = y)$$

Lean4

theorem smul_right_inj [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) {x y : M} : c • x = c • y ↔ x = y :=
  (smul_right_injective M hc).eq_iff

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