lsmul_injective — Mathlib

English

Let A be an algebra over R and M an A-module with NoZeroSmulDivisors. For any nonzero x in A, the map m ↦ x m on M is injective.

Русский

Пусть A — алгебра над R, M — модуль над A, удовлетворяющий условию без нулевых делителей множителя. При любом x ≠ 0 в A левая умножение на x на M инъективно.

LaTeX

$$$\\\\text{If } [NoZeroSmulDivisors A M] \\\\text{ and } x \\\\neq 0, \\\\text{ then } m \\\\mapsto x m \\\\text{ is injective on } M.$$$

Lean4

theorem lsmul_injective [NoZeroSMulDivisors A M] {x : A} (hx : x ≠ 0) : Function.Injective (lsmul R B M x) :=
  smul_right_injective M hx

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