Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_one_class.ext

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 mul_one_class.ext View on Github →