map_bot

Mathlib.Algebra.Group.Subgroup.Map

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

English

If f: G → N is a group homomorphism, the image of the trivial subgroup of G is the trivial subgroup of N.

Русский

Пусть f: G → N — гомоморфизм групп. Образ тривиальной подгруппы G в N равен тривиальной подгруппе N.

LaTeX

$$$ (\\bot_G).map f = \\bot_N $$$

Lean4

@[to_additive (attr := simp)]
theorem map_bot (f : G →* N) : (⊥ : Subgroup G).map f = ⊥ :=
  (gc_map_comap f).l_bot

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

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

Разделы

Аффилиация

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