Mathlib v3 is deprecated. Go to Mathlib v4

Theorem cancel_comm_monoid.to_comm_monoid_injective

Modification history

2021-11-05 13:33
src/algebra/group/defs.lean
refactor(algebra/group): move `monoid.has_pow` etc to `algebra.group.defs` (#10147) …
Modified cancel_comm_monoid.to_comm_monoid_injectiveView on Github →
2021-09-01 05:57
src/algebra/group/defs.lean
feat(algebra/group/defs): ext lemmas for (semi)groups and monoids (#8391) …
Added cancel_comm_monoid.to_comm_monoid_injectiveView on Github →