Theorems · Theorem · group theory

AddMonoidHom.prod_comp_prodMap

∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {M' : Type u_6}
  {N' : Type u_7} [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] [inst_4 : AddZeroClass 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 15 from the axioms · uses propext, Quot.sound

Assumes

AddZeroClassAddZeroClassAddZeroClassAddZeroClassAddZeroClass