range_eq_map

Mathlib.Algebra.Group.Subgroup.Ker

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

English

The image of a monoid hom f: G →* N equals the map of the top subgroup under f; i.e. f.range = (⊤).map f.

Русский

Образ f совпадает с отображением верхней подгруппы через f: f.range = ⊤.map f.

LaTeX

$$$\mathrm{Im}(f) = (\top : \mathrm{Subgroup}(G)).\mathrm{map} \; f$$$

Lean4

@[to_additive]
theorem range_eq_map (f : G →* N) : f.range = (⊤ : Subgroup G).map f := by ext; simp

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

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

Разделы

Аффилиация

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