Theorem mul_invOf_cancel_left'
Modification history
2026-03-03 17:54
Mathlib/Algebra/Group/Invertible/Defs.lean
feat(CategoryTheory/Monoidal/Grp_): a monoid object with invertible homs is a group object (#36002) …
Modified mul_invOf_cancel_left'View on Github →