Commit 2021-11-06 12:54 af36f1a3

View on Github →

chore(algebra/group/ulift): use injective.* to define instances (#10172) Also rename ulift.mul_equiv to mul_equiv.ulift and add some missing instances.

Estimated changes

Modified src/algebra/group/ulift.lean

added def mul_equiv.ulift

deleted def ulift.mul_equiv

Modified src/algebra/module/ulift.lean