Theorems · Definition · group theory

AddMonoidHom.noncommCoprod

{M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} →
      [inst : AddZeroClass M] →
        [inst_1 : AddZeroClass N] →
          [inst_2 : AddMonoid P] →
            (f : M →+ P) → (g : N →+ P) → (∀ (m : M) (n : N), AddCommute (f m) (g n)) → M × N →+ P

Coproduct of two AddMonoidHoms with the same codomain, with a commutation assumption: f.noncommCoprod g (p : M × N) = f p.1 + g p.2. (Noncommutative case; in the commutative case, use AddHom.coprod.)

Defined in

Mathlib.GroupTheory.NoncommCoprod

Cited by

7 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext

Assumes

AddZeroClassAddZeroClassAddMonoid