map_map — Mathlib

English

For subgroups K of G, g: N → P, f: G → N, we have (K.map f).map g = K.map (g ∘ f).

Русский

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

LaTeX

$$$\\mathrm{map}_g(\\mathrm{map}_f(K)) = \\mathrm{map}_{g \\circ f}(K).$$$

Lean4

@[to_additive]
theorem map_map (g : N →* P) (f : G →* N) : (K.map f).map g = K.map (g.comp f) :=
  SetLike.coe_injective <| image_image _ _ _

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