Theorems · Theorem · group theory

AddMonoidHom.comp_assoc

∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [inst : AddZero M] [inst_1 : AddZero N]
  [inst_2 : AddZero P] [inst_3 : AddZero Q] (f : M →+ N) (g : N →+ P) (h : P →+ Q),
  (h.comp g).comp f = h.comp (g.comp f)

Defined in

Mathlib.Algebra.Group.Hom.Defs

Cited by

5 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Quot.sound

Assumes

AddZeroAddZeroAddZeroAddZero