Theorem GrpObj.one_inv

Modification history

2025-09-17 21:07
Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean
feat(Grp_): `η ≫ ι = η` (#29736) …
Added GrpObj.one_invView on Github →