lsmul_injective

Mathlib.LinearAlgebra.BilinearMap

URI: https://scilib.ai/kg/mathlib#LinearMap.lsmul_injective

English

Under NoZeroSMulDivisors, kernel of lsmul at a nonzero a is zero; i.e., lsmul is injective.

Русский

При NoZeroSMulDivisors ядро lsmul в ненулевом a равно нулю; значит, lsmul инъективно.

LaTeX

$$$\ker(\mathrm{lsmul}\; R\; M\; a) = \{0\}$, если a ≠ 0$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru