Theorems · Theorem · category theory

CategoryTheory.Grp.mkIso.congr_simp

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : CategoryTheory.Grp C} (e e_1 : G.X ≅ H.X) (e_e : e = e_1)
  (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
  (mul_f :
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
        CategoryTheory.MonObj.mul),
  CategoryTheory.Grp.mkIso e one_f mul_f = CategoryTheory.Grp.mkIso e_1 ⋯ ⋯

Defined in

Mathlib.CategoryTheory.Monoidal.Grp

Cited by

0 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategory