Theorem invOf_eq_iff_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) …
Added invOf_eq_iff_leftView on Github →