ker_subtype

Mathlib.Algebra.Group.Subgroup.Ker

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

← MathLib Explorer

English

The kernel of the inclusion map H.subtype: H → G is the trivial subgroup.

Русский

Ядро вложения H в G равно тривиальной подгруппе.

LaTeX

$$$\ker(H\hookrightarrow G) = \bot$$$

Lean4

@[to_additive (attr := simp)]
theorem _root_.Subgroup.ker_subtype (H : Subgroup G) : H.subtype.ker = ⊥ :=
  H.subtype.ker_eq_bot_iff.mpr Subtype.coe_injective

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

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

Разделы

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

Аффилиация

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