ker_of

Mathlib.GroupTheory.Abelianization.Defs

URI: https://scilib.ai/kg/mathlib#Abelianization.ker_of

English

The kernel of the canonical projection is exactly the commutator subgroup: ker(of) = [G,G].

Русский

Ядро канонической проекции равно коммутаторной подгруппе: ker(of) = [G,G].

LaTeX

$$$$ \\ker(\\mathrm{of}) = [G,G]. $$$$

Lean4

@[simp]
theorem ker_of : of.ker = commutator G :=
  QuotientGroup.ker_mk' (commutator G)

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

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

Разделы

Аффилиация

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