Theorems · Theorem · group theory

MulHom.prod_comp_prodMap

∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7} [inst : Mul M] [inst_1 : Mul N]
  [inst_2 : Mul M'] [inst_3 : Mul N'] [inst_4 : Mul P] (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)

Defined in

Mathlib.Algebra.Group.Prod

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext

Assumes

MulMulMulMulMul