Theorem GrpObj.one_inv

Modification history

2025-10-30 04:20
Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean
chore(CategoryTheory): namespace `Mon`, `Grp`, etc... (#30786) …
Deleted GrpObj.one_invView on Github →
2025-09-17 21:07
Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean
feat(Grp_): `η ≫ ι = η` (#29736) …
Added GrpObj.one_invView on Github →