smul_right_injective — Mathlib

English

If NoZeroSMulDivisors R M holds, then for any c, the map x ↦ c • x is injective as soon as c ≠ 0.

Русский

Если выполняется NoZeroSMulDivisors R M, то для любого c скалярная карта x ↦ c • x инъективна при условии c ≠ 0.

LaTeX

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

Lean4

theorem smul_right_injective [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) : Function.Injective (c • · : M → M) :=
  (injective_iff_map_eq_zero (smulAddHom R M c)).2 fun _ ha => (smul_eq_zero.mp ha).resolve_left hc

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