prod_comp_prodMap — Mathlib

English

Repeated statement of product map compatibility with composition; (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

theorem prod_comp_prodMap (f : T →ₙ+* R) (g : T →ₙ+* S) (f' : R →ₙ+* R') (g' : S →ₙ+* S') :
    (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g) :=
  rfl

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