ker_inclusion

Mathlib.Algebra.Module.Submodule.Ker

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

English

For p ⊆ p', the kernel of the inclusion map from p to p' is trivial.

Русский

Для p ⊆ p' ядро включения p в p' тривиально.

LaTeX

$$$\ker(\text{inclusion}\,h) = ⊥$$$

Lean4

@[simp]
theorem ker_inclusion (p p' : Submodule R M) (h : p ≤ p') : ker (inclusion h) = ⊥ := by
  rw [inclusion, ker_codRestrict, ker_subtype]

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

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

Разделы

Аффилиация

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