prod_comp_prodMap — Mathlib

English

For f: P →* M, g: P →* N and f': M →* M', g': N →* N', the equality (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g) holds.

Русский

Пусть 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).

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

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