ULift
instances for groups and monoids #
This file defines instances for group, monoid, semigroup and related structures on ULift
types.
(Recall ULift α
is just a "copy" of a type α
in a higher universe.)
We also provide MulEquiv.ulift : ULift R ≃* R
(and its additive analogue).
Equations
Equations
Equations
Equations
Equations
Equations
@[simp]
@[simp]