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≃+* R.

instance ULift.mulZeroClass {α : Type u} [inst : ] :
Equations
instance ULift.distrib {α : Type u} [inst : ] :
Equations
• ULift.distrib = Distrib.mk (_ : ∀ (x x_1 x_2 : ), x * (x_1 + x_2) = x * x_1 + x * x_2) (_ : ∀ (x x_1 x_2 : ), (x + x_1) * x_2 = x * x_2 + x_1 * x_2)
instance ULift.nonUnitalNonAssocSemiring {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance ULift.nonAssocSemiring {α : Type u} [inst : ] :
Equations
• ULift.nonAssocSemiring = let src := ULift.addMonoidWithOne; NonAssocSemiring.mk (_ : ∀ (a : ), 1 * a = a) (_ : ∀ (a : ), a * 1 = a)
instance ULift.nonUnitalSemiring {α : Type u} [inst : ] :
Equations
instance ULift.semiring {α : Type u} [inst : ] :
Equations
• ULift.semiring = let src := ULift.addMonoidWithOne; Semiring.mk (_ : ∀ (a : ), 1 * a = a) (_ : ∀ (a : ), a * 1 = a) Monoid.npow
def ULift.ringEquiv {α : Type u} [inst : ] :
≃+* α

The ring equivalence between ULift α and α.

Equations
• One or more equations did not get rendered due to their size.
instance ULift.nonUnitalCommSemiring {α : Type u} [inst : ] :
Equations
instance ULift.commSemiring {α : Type u} [inst : ] :
Equations
• ULift.commSemiring = let src := ULift.semiring; CommSemiring.mk (_ : ∀ (a b : ), a * b = b * a)
instance ULift.nonUnitalNonAssocRing {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance ULift.nonUnitalRing {α : Type u} [inst : ] :
Equations
instance ULift.nonAssocRing {α : Type u} [inst : ] :
Equations
instance ULift.ring {α : Type u} [inst : Ring α] :
Ring ()
Equations
• ULift.ring = Ring.mk SubNegMonoid.zsmul (_ : ∀ (a : ), -a + a = 0)
instance ULift.nonUnitalCommRing {α : Type u} [inst : ] :
Equations
instance ULift.commRing {α : Type u} [inst : ] :
Equations
• ULift.commRing = let src := ULift.ring; CommRing.mk (_ : ∀ (a b : ), a * b = b * a)