smul_left_injective — Mathlib

English

If x ≠ 0 in a module M, then the map c ↦ c • x from R to M is injective.

Русский

Если x ≠ 0 в модуле M, то отображение c ↦ c • x из R в M инъективно.

LaTeX

$$Injective (\lambda c:\, c \cdot x)$$

Lean4

theorem smul_left_injective {x : M} (hx : x ≠ 0) : Function.Injective fun c : R => c • x := fun c d h =>
  sub_eq_zero.mp
    ((smul_eq_zero.mp
          (calc
            (c - d) • x = c • x - d • x := sub_smul c d x
            _ = 0 := sub_eq_zero.mpr h)).resolve_right
      hx)

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