Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-12 00:24 f6c8d81c

View on Github →

feat(algebra/group/with_one): Use an equiv for lift (#4975)

Estimated changes

modified def with_one.lift