ker_lsmul

Mathlib.LinearAlgebra.BilinearMap

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

← MathLib Explorer

English

If a ≠ 0, ker(lsmul) = ⊥, i.e., lsmul has trivial kernel.

Русский

Если a ≠ 0, ker(lsmul) = ⊥, то ядро lsmul тривиально.

LaTeX

$$$\ker(\mathrm{lsmul}\; R\; M\; a) = \bot$ when $a \neq 0$$$

Lean4

theorem ker_lsmul [NoZeroSMulDivisors R M] {a : R} (ha : a ≠ 0) : LinearMap.ker (LinearMap.lsmul R M a) = ⊥ :=
  LinearMap.ker_eq_bot_of_injective (LinearMap.lsmul_injective ha)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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