ULift
instances for ring #
This file defines instances for ring, semiring and related structures on ULift
types.
(Recall ULift α
is just a "copy" of a type α
in a higher universe.)
We also provide ULift.ringEquiv : ULift R ≃+* R≃+* R
.
Equations
- One or more equations did not get rendered due to their size.
The ring equivalence between ULift α
and α
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.