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.

source
instance ULift.mulZeroClass {α : Type u} [MulZeroClass α] :
MulZeroClass (ULift.{u_1, u} α)
Equations
source
instance ULift.distrib {α : Type u} [Distrib α] :
Distrib (ULift.{u_1, u} α)
Equations
source
instance ULift.nonUnitalNonAssocSemiring {α : Type u} [NonUnitalNonAssocSemiring α] :
NonUnitalNonAssocSemiring (ULift.{u_1, u} α)
Equations
source
instance ULift.nonAssocSemiring {α : Type u} [NonAssocSemiring α] :
NonAssocSemiring (ULift.{u_1, u} α)
Equations
source
instance ULift.nonUnitalSemiring {α : Type u} [NonUnitalSemiring α] :
NonUnitalSemiring (ULift.{u_1, u} α)
Equations
source
instance ULift.semiring {α : Type u} [Semiring α] :
Semiring (ULift.{u_1, u} α)
Equations
  • ULift.semiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯
source
def ULift.ringEquiv {α : Type u} [NonUnitalNonAssocSemiring α] :
ULift.{u_1, u} α ≃+* α

The ring equivalence between ULift α and α.

Equations
  • ULift.ringEquiv = { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
Instances For
    source
    instance ULift.nonUnitalCommSemiring {α : Type u} [NonUnitalCommSemiring α] :
    NonUnitalCommSemiring (ULift.{u_1, u} α)
    Equations
    source
    instance ULift.commSemiring {α : Type u} [CommSemiring α] :
    CommSemiring (ULift.{u_1, u} α)
    Equations
    source
    instance ULift.nonUnitalNonAssocRing {α : Type u} [NonUnitalNonAssocRing α] :
    NonUnitalNonAssocRing (ULift.{u_1, u} α)
    Equations
    source
    instance ULift.nonUnitalRing {α : Type u} [NonUnitalRing α] :
    NonUnitalRing (ULift.{u_1, u} α)
    Equations
    source
    instance ULift.nonAssocRing {α : Type u} [NonAssocRing α] :
    NonAssocRing (ULift.{u_1, u} α)
    Equations
    source
    instance ULift.ring {α : Type u} [Ring α] :
    Ring (ULift.{u_1, u} α)
    Equations
    • ULift.ring = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
    source
    instance ULift.nonUnitalCommRing {α : Type u} [NonUnitalCommRing α] :
    NonUnitalCommRing (ULift.{u_1, u} α)
    Equations
    source
    instance ULift.commRing {α : Type u} [CommRing α] :
    CommRing (ULift.{u_1, u} α)
    Equations