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.

ink

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

Equations

• ULift.mulZeroClass = MulZeroClass.mk (_ : ∀ (x : ULift α), 0 * x = 0) (_ : ∀ (x : ULift α), x * 0 = 0)

ink

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

Equations

• ULift.distrib = Distrib.mk (_ : ∀ (x x_1 x_2 : ULift α), x * (x_1 + x_2) = x * x_1 + x * x_2) (_ : ∀ (x x_1 x_2 : ULift α), (x + x_1) * x_2 = x * x_2 + x_1 * x_2)

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• ULift.nonAssocSemiring = let src := ULift.addMonoidWithOne; NonAssocSemiring.mk (_ : ∀ (a : ULift α), 1 * a = a) (_ : ∀ (a : ULift α), a * 1 = a)

ink

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

Equations

• ULift.nonUnitalSemiring = NonUnitalSemiring.mk (_ : ∀ (a b c : ULift α), a * b * c = a * (b * c))

ink

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

Equations

• ULift.semiring = let src := ULift.addMonoidWithOne; Semiring.mk (_ : ∀ (a : ULift α), 1 * a = a) (_ : ∀ (a : ULift α), a * 1 = a) Monoid.npow

ink

def ULift.ringEquiv {α : Type u} [inst : NonUnitalNonAssocSemiring α] : ULift α ≃+* α

The ring equivalence between ULift α and α.

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• ULift.nonUnitalCommSemiring = NonUnitalCommSemiring.mk (_ : ∀ (a b : ULift α), a * b = b * a)

ink

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

Equations

• ULift.commSemiring = let src := ULift.semiring; CommSemiring.mk (_ : ∀ (a b : ULift α), a * b = b * a)

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• ULift.nonUnitalRing = NonUnitalRing.mk (_ : ∀ (a b c : ULift α), a * b * c = a * (b * c))

ink

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

Equations

• ULift.nonAssocRing = NonAssocRing.mk (_ : ∀ (a : ULift α), 1 * a = a) (_ : ∀ (a : ULift α), a * 1 = a)

ink

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

Equations

• ULift.ring = Ring.mk SubNegMonoid.zsmul (_ : ∀ (a : ULift α), -a + a = 0)

ink

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

Equations

• ULift.nonUnitalCommRing = NonUnitalCommRing.mk (_ : ∀ (a b : ULift α), a * b = b * a)

ink

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

Equations

• ULift.commRing = let src := ULift.ring; CommRing.mk (_ : ∀ (a b : ULift α), a * b = b * a)