Def CategoryTheory.GrpObj.ofInvertible

Modification history

2026-03-03 17:54
Mathlib/CategoryTheory/Monoidal/Grp_.lean
feat(CategoryTheory/Monoidal/Grp_): a monoid object with invertible homs is a group object (#36002) …
Added CategoryTheory.GrpObj.ofInvertibleView on Github →