ker_subtype

Mathlib.Algebra.Module.Submodule.Ker

URI: https://scilib.ai/kg/mathlib#Submodule.ker_subtype

English

The kernel of the inclusion map p.subtype: p → M is trivial.

Русский

Ядро включения p.subtype: p → M тривиально.

LaTeX

$$$\ker(p\,\text{subtype}) = ⊥$$$

Lean4

@[simp]
theorem ker_subtype : ker p.subtype = ⊥ :=
  ker_eq_bot_of_injective fun _ _ => Subtype.ext

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

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

Разделы

Аффилиация

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