ker_mk'

Mathlib.GroupTheory.QuotientGroup.Defs

URI: https://scilib.ai/kg/mathlib#QuotientGroup.ker_mk'

English

The kernel of the quotient map mk' : G → G/N is exactly N.

Русский

Ядро сопоставления mk' : G → G/N равно N.

LaTeX

$$$ \ker( \operatorname{QuotientGroup.mk'}(N) : G \to G / N ) = N $$$

Lean4

@[to_additive (attr := simp)]
theorem ker_mk' : MonoidHom.ker (QuotientGroup.mk' N : G →* G ⧸ N) = N :=
  Subgroup.ext eq_one_iff

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

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

Разделы

Аффилиация

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