ker_rangeRestrict

Mathlib.Algebra.Group.Subgroup.Ker

URI: https://scilib.ai/kg/mathlib#MonoidHom.ker_rangeRestrict

English

The kernel of the rangeRestrict map equals the kernel of f.

Русский

Ядро отображения rangeRestrict совпадает с ядром f.

LaTeX

$$$$ \\ker(\\mathrm{rangeRestrict}\\,f) = \\ker f $$$$

Lean4

@[to_additive (attr := simp)]
theorem ker_rangeRestrict (f : G →* N) : ker (rangeRestrict f) = ker f :=
  ker_codRestrict _ _ _

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

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

Разделы

Аффилиация

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