Theorems · Theorem · group theory

MulHom.prodMap_def

∀ {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul M']
  [inst_3 : Mul N'] (f : M →ₙ* M') (g : N →ₙ* N'),
  f.prodMap g = (f.comp (MulHom.fst M N)).prod (g.comp (MulHom.snd M N))

Defined in

Mathlib.Algebra.Group.Prod

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext

Assumes

MulMulMulMul