Theorems · Theorem · category theory

CategoryTheory.CommRingObjCat.Hom.mk.inj

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {R₁ R₂ : CategoryTheory.CommRingObjCat C} {hom : R₁.X ⟶ R₂.X}
  {isRingHom : CategoryTheory.IsRingHom hom} {hom_1 : R₁.X ⟶ R₂.X} {isRingHom_1 : CategoryTheory.IsRingHom hom_1},
  { hom := hom, isRingHom := isRingHom } = { hom := hom_1, isRingHom := isRingHom_1 } → hom = hom_1

Defined in

Mathlib.CategoryTheory.Monoidal.Ring

Cited by

1 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms