Mathlib v3 is deprecated. Go to Mathlib v4

Def mul_equiv.ulift

Modification history

2021-11-06 12:54

src/algebra/group/ulift.lean

chore(algebra/group/ulift): use injective.* to define instances (#10172) …

Added mul_equiv.ulift View on Github →