map_comp

Mathlib.GroupTheory.Abelianization.Defs

URI: https://scilib.ai/kg/mathlib#Abelianization.map_comp

English

For f: G →* H and g: H →* I, we have map_g ∘ map_f = map_{g ∘ f}.

Русский

Для гомоморфизмов f: G →* H и g: H →* I имеет место map_g ∘ map_f = map_{g ∘ f}.

LaTeX

$$$$ (\\mathrm{map} \\, g) \\circ (\\mathrm{map} \\, f) = \\mathrm{map}(g \\circ f). $$$$

Lean4

@[simp]
theorem map_comp {I : Type w} [Group I] (g : H →* I) : (map g).comp (map f) = map (g.comp f) :=
  hom_ext _ _ rfl

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

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

Разделы

Аффилиация

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