Theorems · Theorem · category theory

CategoryTheory.AddMon.Hom.mk.injEq

∀ {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

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.IsAddMonHom