Mathlib v3 is deprecated. Go to Mathlib v4

Theorem comm_group.to_group_injective

Modification history

2021-09-01 05:57
src/algebra/group/defs.lean
feat(algebra/group/defs): ext lemmas for (semi)groups and monoids (#8391) …
Added comm_group.to_group_injectiveView on Github →