prod_comp_prodMap — Mathlib

English

For f,g with appropriate types, (f' × g') ∘ (f × g) = (f' ∘ f) × (g' ∘ g).

Русский

Для совместимых отображений выполняется (f' × g') ∘ (f × g) = (f' ∘ f) × (g' ∘ 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

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