Documentation

Mathlib.Algebra.Ring.ULift

ULift instances for ring #

This file defines instances for ring, semiring and related structures on ULift types.

(Recall ULift R is just a "copy" of a type R in a higher universe.)

We also provide ULift.ringEquiv : ULift R ≃+* R.

Equations
instance ULift.distrib {R : Type u} [Distrib R] :
Equations
Equations
Equations
@[simp]
theorem ULift.up_natCast {R : Type u} [NatCast R] (n : ) :
{ down := n } = n
@[simp]
theorem ULift.up_ofNat {R : Type u} [NatCast R] (n : ) [n.AtLeastTwo] :
@[simp]
theorem ULift.up_intCast {R : Type u} [IntCast R] (n : ) :
{ down := n } = n
@[simp]
theorem ULift.down_natCast {R : Type u} [NatCast R] (n : ) :
(↑n).down = n
@[simp]
theorem ULift.down_ofNat {R : Type u} [NatCast R] (n : ) [n.AtLeastTwo] :
@[simp]
theorem ULift.down_intCast {R : Type u} [IntCast R] (n : ) :
(↑n).down = n
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.

The ring equivalence between ULift R and R.

Equations
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    instance ULift.ring {R : Type u} [Ring R] :
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations