ker_le_comap

Mathlib.Algebra.Group.Subgroup.Ker

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

English

For a MonoidHom f and a subgroup H of G', ker f is contained in the preimage under f of H.

Русский

Для моноидного гомоморфизма f и подгруппы H образа G', ядро f лежит в обратном образе H.

LaTeX

$$$f.ker \le \mathrm{comap}_f(H)$$$

Lean4

@[to_additive]
theorem ker_le_comap (H : Subgroup N) : f.ker ≤ comap f H :=
  comap_bot f ▸ comap_mono bot_le

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

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

Разделы

Аффилиация

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