map_eq_range_iff

Mathlib.Algebra.Group.Subgroup.Ker

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

← MathLib Explorer

English

Let f: G → N. Then H.map f = f.range iff Codisjoint H ker f.

Русский

Пусть f: G → N. Тогда H.map f = f.range тогда и только тогда, когда Codisjoint(H, ker f).

LaTeX

$$$H.map f = f.range \\iff Codisjoint(H, \\ker f)$$$

Lean4

@[to_additive]
theorem map_eq_range_iff {f : G →* N} {H : Subgroup G} : H.map f = f.range ↔ Codisjoint H f.ker := by
  rw [f.range_eq_map, map_eq_map_iff, codisjoint_iff, top_sup_eq]

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

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

Разделы

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

Аффилиация

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