Theorems · Theorem · category theory

CategoryTheory.AddMon.Hom.mk.inj

∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {M N : CategoryTheory.AddMon C} {hom : M.X ⟶ N.X} {isAddMonHom_hom : CategoryTheory.IsAddMonHom hom}
  {hom_1 : M.X ⟶ N.X} {isAddMonHom_hom_1 : CategoryTheory.IsAddMonHom hom_1},
  { hom := hom, isAddMonHom_hom := isAddMonHom_hom } = { hom := hom_1, isAddMonHom_hom := isAddMonHom_hom_1 } →
    hom = hom_1

Defined in

Mathlib.CategoryTheory.Monoidal.Mon

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms