Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-01 05:57 f0451d80

View on Github →

feat(algebra/group/defs): ext lemmas for (semi)groups and monoids (#8391) Zulip discussion

Estimated changes

Modified src/algebra/group/defs.lean

added theorem cancel_comm_monoid.ext

added theorem cancel_comm_monoid.to_comm_monoid_injective

added theorem cancel_monoid.ext

added theorem cancel_monoid.to_left_cancel_monoid_injective

added theorem comm_group.ext

added theorem comm_group.to_group_injective

added theorem comm_monoid.ext

added theorem comm_monoid.to_monoid_injective

added theorem div_inv_monoid.ext

added theorem group.ext

added theorem group.to_div_inv_monoid_injective

added theorem left_cancel_monoid.ext

added theorem left_cancel_monoid.to_monoid_injective

added theorem monoid.ext

added theorem mul_one_class.ext

added theorem right_cancel_monoid.ext

added theorem right_cancel_monoid.to_monoid_injective

Modified src/category_theory/preadditive/schur.lean

Modified test/equiv_rw.lean