Commit 2025-03-05 17:48 1fb7412a

View on Github →

feat(CategoryTheory): API for group objects (#22168)

Estimated changes

Modified Mathlib/CategoryTheory/ChosenFiniteProducts.lean

added theorem CategoryTheory.ChosenFiniteProducts.comp_toUnit

added theorem CategoryTheory.ChosenFiniteProducts.lift_snd_fst

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

added theorem Grp_.inv_comp_inv

added theorem Grp_.inv_inv

added theorem Grp_.lift_left_mul_ext

added def Grp_.mk'

added def Grp_.mulRight

added theorem Grp_.mulRight_one

added theorem Grp_.mul_inv

added theorem Grp_.tensorHom_inv_inv_mul

added theorem Grp_Class.ext

added theorem Grp_Class.left_inv

added theorem Grp_Class.right_inv

added theorem Grp_Class.toMon_Class_injective

added theorem IsMon_Hom.inv_hom

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

added theorem Mon_Class.ext

Modified Mathlib/CategoryTheory/Monoidal/Yoneda.lean