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 : MulZeroClass α] :
Equations
instance ULift.distrib {α : Type u} [inst : Distrib α] :
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)
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
instance ULift.semiring {α : Type u} [inst : Semiring α] :
Equations
  • ULift.semiring = let src := ULift.addMonoidWithOne; Semiring.mk (_ : ∀ (a : ULift α), 1 * a = a) (_ : ∀ (a : ULift α), a * 1 = a) Monoid.npow
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.
Equations
instance ULift.commSemiring {α : Type u} [inst : CommSemiring α] :
Equations
Equations
  • One or more equations did not get rendered due to their size.
instance ULift.nonUnitalRing {α : Type u} [inst : NonUnitalRing α] :
Equations
instance ULift.nonAssocRing {α : Type u} [inst : NonAssocRing α] :
Equations
instance ULift.ring {α : Type u} [inst : Ring α] :
Ring (ULift α)
Equations
Equations
instance ULift.commRing {α : Type u} [inst : CommRing α] :
Equations