Mathlib v3 is deprecated. Go to Mathlib v4

Def ulift.mul_equiv

Modification history

2021-11-06 12:54
src/algebra/group/ulift.lean
chore(algebra/group/ulift): use injective.* to define instances (#10172) …
Deleted ulift.mul_equivView on Github →
2021-04-19 09:07
src/algebra/group/ulift.lean
chore(algebra/group): missed generalizations to mul_one_class (#7259) …
Modified ulift.mul_equivView on Github →
2020-08-05 11:37
src/algebra/group/ulift.lean
feat(algebra/*/ulift): algebraic instances for ulift (#3675)
Added ulift.mul_equivView on Github →