ker_id

Mathlib.Algebra.Module.Submodule.Ker

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

English

The kernel of the identity map is trivial; it contains only the zero vector.

Русский

Ядро тождественного отображения тривиально; содержит только нулевой вектор.

LaTeX

$$$\ker(\mathrm{id}_M) = \{0\}$$$

Lean4

@[simp]
theorem ker_id : ker (LinearMap.id : M →ₗ[R] M) = ⊥ :=
  rfl

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

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

Разделы

Аффилиация

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