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]
Equations
- ulift.mul_zero_class = {mul := has_mul.mul ulift.has_mul, zero := 0, zero_mul := _, mul_zero := _}
@[instance]
Equations
- ulift.distrib = {mul := has_mul.mul ulift.has_mul, add := has_add.add ulift.has_add, left_distrib := _, right_distrib := _}
@[instance]
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 := _}
@[instance]
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]
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]
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 := _}