Theorem GrpObj.tensorObj.CategoryTheory.Functor.obj.ι_def

Modification history

2025-10-30 04:20
Mathlib/CategoryTheory/Monoidal/Grp_.lean
chore(CategoryTheory): namespace `Mon`, `Grp`, etc... (#30786) …
Deleted GrpObj.tensorObj.CategoryTheory.Functor.obj.ι_defView on Github →
2025-09-17 21:07
Mathlib/CategoryTheory/Monoidal/Grp_.lean
feat: pushforward of a group object along a monoidal functor (#29691) …
Added GrpObj.tensorObj.CategoryTheory.Functor.obj.ι_defView on Github →