Theorems · Definition · group theory

MulEquiv.coprodAssoc

(M : Type u_1) →
  (N : Type u_2) →
    (P : Type u_3) →
      [inst : Monoid M] →
        [inst_1 : Monoid N] →
          [inst_2 : Monoid P] → Monoid.Coprod (Monoid.Coprod M N) P ≃* Monoid.Coprod M (Monoid.Coprod N P)

A multiplicative equivalence between (M ∗ N) ∗ P and M ∗ (N ∗ P).

Defined in: Mathlib.GroupTheory.Coprod.Basic
Cited by: 6 results in Mathlib
Foundations: Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Monoid Monoid Monoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Monoidstatement and proof · cited by 3,887
MulEquivstatement · cited by 1,142
MonoidHom.compproof · cited by 469
MonoidHom.idproof · cited by 323
Monoid.Coprodstatement · cited by 109
Monoid.Coprod.inlproof · cited by 48
Monoid.Coprod.inrproof · cited by 47
Monoid.Coprod.liftproof · cited by 13
Monoid.Coprod.mapproof · cited by 12
MonoidHom.toMulEquivproof · cited by 3

Cited by6

Results whose statement or proof uses this declaration.

MulEquiv.coprodAssoc_apply_inl_inlstatement · cited by 0
MulEquiv.coprodAssoc_apply_inl_inrstatement · cited by 0
MulEquiv.coprodAssoc_apply_inrstatement · cited by 0
MulEquiv.coprodAssoc_symm_apply_inlstatement · cited by 0
MulEquiv.coprodAssoc_symm_apply_inr_inlstatement · cited by 0
MulEquiv.coprodAssoc_symm_apply_inr_inrstatement · cited by 0