Commit 2026-03-03 17:54 753a220b

View on Github →

feat(CategoryTheory/Monoidal/Grp_): a monoid object with invertible homs is a group object (#36002) This PR constructs a group object from a monoid object with invertible homs.

Estimated changes

modified theorem Invertible.congr
added theorem invOf_eq_iff_left
added theorem invOf_eq_iff_right
modified theorem invOf_eq_left_inv
modified theorem invOf_eq_right_inv
modified theorem invOf_mul_cancel_left'
modified theorem invOf_mul_cancel_left
modified theorem invOf_mul_cancel_right'
modified theorem invOf_mul_cancel_right
modified theorem invertible_unique
modified theorem mul_invOf_cancel_left'
modified theorem mul_invOf_cancel_left
modified theorem mul_invOf_cancel_right'
modified theorem mul_invOf_cancel_right