Documentation

Mathlib.Algebra.Ring.ULift

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.

Equations
instance ULift.distrib {α : Type u} [Distrib α] :
Equations
Equations
Equations
Equations
instance ULift.semiring {α : Type u} [Semiring α] :
Equations
  • ULift.semiring = let __src := ULift.addMonoidWithOne; Semiring.mk Monoid.npow

The ring equivalence between ULift α and α.

Equations
  • ULift.ringEquiv = { toEquiv := { toFun := ULift.down, invFun := ULift.up, left_inv := , right_inv := }, map_mul' := , map_add' := }
Instances For
    Equations
    Equations
    Equations
    Equations
    instance ULift.ring {α : Type u} [Ring α] :
    Equations
    • ULift.ring = Ring.mk SubNegMonoid.zsmul
    Equations
    instance ULift.commRing {α : Type u} [CommRing α] :
    Equations