prod_comp_prodMap — Mathlib

English

Compatibilities between prodMap and composition with prod: prod_comp_prodMap expresses equality of composite maps.

Русский

Согласованности между prodMap и композициями с prod задают равенство составных отображений.

LaTeX

$$$(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)$$$

Lean4

@[to_additive prod_comp_prodMap]
theorem prod_comp_prodMap (f : P →ₙ* M) (g : P →ₙ* N) (f' : M →ₙ* M') (g' : N →ₙ* N') :
    (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g) :=
  rfl

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