Theorems · Theorem · category theory

CategoryTheory.RingObjCat.mk.inj

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {X : C} {ringObj : CategoryTheory.RingObj X} {X_1 : C}
  {ringObj_1 : CategoryTheory.RingObj X_1},
  { X := X, ringObj := ringObj } = { X := X_1, ringObj := ringObj_1 } → X = X_1 ∧ ringObj ≍ ringObj_1

Defined in

Mathlib.CategoryTheory.Monoidal.Ring

Cited by

1 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms