ker_inclusion

Mathlib.Algebra.Group.Subgroup.Ker

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

← MathLib Explorer

English

If H ≤ K, the kernel of the inclusion map H → K is trivial.

Русский

Если H ≤ K, ядро включения H → K тривиально.

LaTeX

$$$\ker(\iota_{H\to K}) = \bot$$$

Lean4

@[to_additive (attr := simp)]
theorem _root_.Subgroup.ker_inclusion {H K : Subgroup G} (h : H ≤ K) : (inclusion h).ker = ⊥ :=
  (inclusion h).ker_eq_bot_iff.mpr (Set.inclusion_injective h)

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

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

Разделы

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

Аффилиация

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