Theorems · Definition · group theory

AddEquiv.coprodAssoc

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

An additive equivalence between AddMonoid.Coprod (AddMonoid.Coprod M N) P and AddMonoid.Coprod M (AddMonoid.Coprod 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: AddMonoid AddMonoid AddMonoid

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.

AddMonoidstatement and proof · cited by 2,864
AddEquivstatement · cited by 1,087
AddMonoidHom.compproof · cited by 339
AddMonoidHom.idproof · cited by 107
AddMonoid.Coprodstatement · cited by 104
AddMonoid.Coprod.inlproof · cited by 42
AddMonoid.Coprod.inrproof · cited by 42
AddMonoid.Coprod.liftproof · cited by 13
AddMonoid.Coprod.mapproof · cited by 12
AddMonoidHom.toAddEquivproof · cited by 3

Cited by6

Results whose statement or proof uses this declaration.

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