mathlib
f6c8d81c - feat(algebra/group/with_one): Use an equiv for `lift` (#4975)

Commit

5 years ago

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

Author

eric-wieser

eric-wieser

Parents

Loading