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.

instance ULift.mulZeroClass {α : Type u} [MulZeroClass α] : MulZeroClass (ULift.{u_1, u} α)

Equations

• ULift.mulZeroClass = MulZeroClass.mk ⋯ ⋯

instance ULift.distrib {α : Type u} [Distrib α] : Distrib (ULift.{u_1, u} α)

Equations

• ULift.distrib = Distrib.mk ⋯ ⋯

instance ULift.nonUnitalNonAssocSemiring {α : Type u} [NonUnitalNonAssocSemiring α] : NonUnitalNonAssocSemiring (ULift.{u_1, u} α)

Equations

• ULift.nonUnitalNonAssocSemiring = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

instance ULift.nonAssocSemiring {α : Type u} [NonAssocSemiring α] : NonAssocSemiring (ULift.{u_1, u} α)

Equations

• ULift.nonAssocSemiring = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

instance ULift.nonUnitalSemiring {α : Type u} [NonUnitalSemiring α] : NonUnitalSemiring (ULift.{u_1, u} α)

Equations

• ULift.nonUnitalSemiring = NonUnitalSemiring.mk ⋯

instance ULift.semiring {α : Type u} [Semiring α] : Semiring (ULift.{u_1, u} α)

Equations

• ULift.semiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯

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' := ⋯ }

instance ULift.nonUnitalCommSemiring {α : Type u} [NonUnitalCommSemiring α] : NonUnitalCommSemiring (ULift.{u_1, u} α)

Equations

• ULift.nonUnitalCommSemiring = NonUnitalCommSemiring.mk ⋯

instance ULift.commSemiring {α : Type u} [CommSemiring α] : CommSemiring (ULift.{u_1, u} α)

Equations

• ULift.commSemiring = CommSemiring.mk ⋯

instance ULift.nonUnitalNonAssocRing {α : Type u} [NonUnitalNonAssocRing α] : NonUnitalNonAssocRing (ULift.{u_1, u} α)

Equations

• ULift.nonUnitalNonAssocRing = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯

instance ULift.nonUnitalRing {α : Type u} [NonUnitalRing α] : NonUnitalRing (ULift.{u_1, u} α)

Equations

• ULift.nonUnitalRing = NonUnitalRing.mk ⋯

instance ULift.nonAssocRing {α : Type u} [NonAssocRing α] : NonAssocRing (ULift.{u_1, u} α)

Equations

• ULift.nonAssocRing = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ULift.ring {α : Type u} [Ring α] : Ring (ULift.{u_1, u} α)

Equations

• ULift.ring = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ULift.nonUnitalCommRing {α : Type u} [NonUnitalCommRing α] : NonUnitalCommRing (ULift.{u_1, u} α)

Equations

• ULift.nonUnitalCommRing = NonUnitalCommRing.mk ⋯

instance ULift.commRing {α : Type u} [CommRing α] : CommRing (ULift.{u_1, u} α)

Equations

• ULift.commRing = CommRing.mk ⋯