range_comp

Mathlib.Algebra.Group.Subgroup.Ker

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

English

For monoid homomorphisms g: N →* P and f: G →* N, (g ∘ f).range = f.range.map g.

Русский

Для гомоморфизмов g: N →* P и f: G →* N выполняется (g ∘ f).range = f.range.map g.

LaTeX

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

Lean4

@[to_additive]
theorem range_comp (g : N →* P) (f : G →* N) : (g.comp f).range = f.range.map g :=
  (map_range ..).symm

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

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

Разделы

Аффилиация

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