mathlib documentation

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.

@[instance]

def ulift.mul_zero_class {α : Type u} [mul_zero_class α] :

mul_zero_class (ulift α)

Equations

ulift.mul_zero_class = {mul := has_mul.mul ulift.has_mul, zero := 0, zero_mul := _, mul_zero := _}

@[instance]

def ulift.distrib {α : Type u} [distrib α] :

distrib (ulift α)

Equations

ulift.distrib = {mul := has_mul.mul ulift.has_mul, add := has_add.add ulift.has_add, left_distrib := _, right_distrib := _}

@[instance]

def ulift.semiring {α : Type u} [semiring α] :

semiring (ulift α)

Equations

ulift.semiring = {add := has_add.add ulift.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, add_comm := _, mul := has_mul.mul ulift.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}

def ulift.ring_equiv {α : Type u} [semiring α] :

ulift α ≃+* α

The ring equivalence between ulift α and α.

Equations

ulift.ring_equiv = {to_fun := ulift.down α, inv_fun := ulift.up α, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

@[instance]

def ulift.comm_semiring {α : Type u} [comm_semiring α] :

comm_semiring (ulift α)

Equations

ulift.comm_semiring = {add := has_add.add ulift.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, add_comm := _, mul := has_mul.mul ulift.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}

@[instance]

def ulift.ring {α : Type u} [ring α] :

ring (ulift α)

Equations

ulift.ring = {add := has_add.add ulift.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg ulift.has_neg, add_left_neg := _, add_comm := _, mul := has_mul.mul ulift.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}

@[instance]

def ulift.comm_ring {α : Type u} [comm_ring α] :

comm_ring (ulift α)

Equations

ulift.comm_ring = {add := has_add.add ulift.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg ulift.has_neg, add_left_neg := _, add_comm := _, mul := has_mul.mul ulift.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}