# mathlibdocumentation

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

@[protected, instance]
def ulift.mul_zero_class {α : Type u}  :
Equations
@[protected, instance]
def ulift.distrib {α : Type u} [distrib α] :
Equations
@[protected, instance]
def ulift.non_unital_non_assoc_semiring {α : Type u}  :
Equations
@[protected, instance]
def ulift.non_assoc_semiring {α : Type u}  :
Equations
@[protected, instance]
def ulift.non_unital_semiring {α : Type u}  :
Equations
@[protected, instance]
def ulift.semiring {α : Type u} [semiring α] :
Equations
def ulift.ring_equiv {α : Type u}  :
≃+* α

The ring equivalence between ulift α and α.

Equations
@[protected, instance]
def ulift.non_unital_comm_semiring {α : Type u}  :
Equations
@[protected, instance]
def ulift.comm_semiring {α : Type u}  :
Equations
@[protected, instance]
def ulift.non_unital_non_assoc_ring {α : Type u}  :
Equations
@[protected, instance]
def ulift.non_unital_ring {α : Type u}  :
Equations
@[protected, instance]
def ulift.non_assoc_ring {α : Type u}  :
Equations
@[protected, instance]
def ulift.ring {α : Type u} [ring α] :
ring (ulift α)
Equations
@[protected, instance]
def ulift.non_unital_comm_ring {α : Type u}  :
Equations
@[protected, instance]
def ulift.comm_ring {α : Type u} [comm_ring α] :
Equations
@[protected, instance]
def ulift.has_rat_cast {α : Type u} [has_rat_cast α] :
Equations
@[simp]
theorem ulift.rat_cast_down {α : Type u} [has_rat_cast α] (n : ) :
@[protected, instance]
def ulift.field {α : Type u} [field α] :
Equations