Theorems · Definition · group theory

MulHom.noncommCoprod

{M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} →
      [inst : Mul M] →
        [inst_1 : Mul N] →
          [inst_2 : Semigroup P] →
            (f : M →ₙ* P) → (g : N →ₙ* P) → (∀ (m : M) (n : N), Commute (f m) (g n)) → M × N →ₙ* P

Coproduct of two MulHoms with the same codomain with Commute assumption: f.noncommCoprod g _ (p : M × N) = f p.1 * g p.2. (For the commutative case, use MulHom.coprod)

Defined in

Mathlib.GroupTheory.NoncommCoprod

Cited by

3 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext

Assumes

MulMulSemigroup