ker_eq_bot

Mathlib.Algebra.Lie.Ideal

URI: https://scilib.ai/kg/mathlib#LieHom.ker_eq_bot

← MathLib Explorer

English

Kernel is zero iff f is injective.

Русский

Ядро равно нулю тогда и только тогда, когда f инъективно.

LaTeX

$$$f.ker = \\{0\\} \\iff \\text{Injective}(f)$$

Lean4

theorem ker_eq_bot : f.ker = ⊥ ↔ Function.Injective f := by
  rw [← LieSubmodule.toSubmodule_inj, ker_toSubmodule, LieSubmodule.bot_toSubmodule, LinearMap.ker_eq_bot,
    coe_toLinearMap]

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

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

Разделы

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

Аффилиация

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