Theorems · Definition · category theory

CategoryTheory.CommRingObjCat.Hom.mk.noConfusion

{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.CartesianMonoidalCategory C} →
      {inst_2 : CategoryTheory.BraidedCategory C} →
        {R₁ R₂ : CategoryTheory.CommRingObjCat C} →
          {P : Sort u_1} →
            {hom : R₁.X ⟶ R₂.X} →
              {isRingHom : CategoryTheory.IsRingHom hom} →
                {hom' : R₁.X ⟶ R₂.X} →
                  {isRingHom' : CategoryTheory.IsRingHom hom'} →
                    { hom := hom, isRingHom := isRingHom } = { hom := hom', isRingHom := isRingHom' } →
                      (hom ≍ hom' → P) → P

Defined in

Mathlib.CategoryTheory.Monoidal.Ring

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms