ulift instances for ring #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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]
Equations
- ulift.mul_zero_class = {mul := has_mul.mul ulift.has_mul, zero := 0, zero_mul := _, mul_zero := _}
@[protected, instance]
Equations
- ulift.distrib = {mul := has_mul.mul ulift.has_mul, add := has_add.add ulift.has_add, left_distrib := _, right_distrib := _}
@[protected, instance]
Equations
- ulift.non_unital_non_assoc_semiring = {add := has_add.add ulift.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul ulift.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul ulift.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
@[protected, instance]
Equations
- ulift.non_assoc_semiring = {add := has_add.add ulift.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul ulift.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul ulift.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := 1, one_mul := _, mul_one := _, nat_cast := add_monoid_with_one.nat_cast ulift.add_monoid_with_one, nat_cast_zero := _, nat_cast_succ := _}
@[protected, instance]
Equations
- ulift.non_unital_semiring = {add := has_add.add ulift.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul ulift.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul ulift.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
@[protected, instance]
Equations
- ulift.semiring = {add := has_add.add ulift.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul ulift.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul ulift.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, nat_cast := add_monoid_with_one.nat_cast ulift.add_monoid_with_one, nat_cast_zero := _, nat_cast_succ := _, npow := monoid.npow ulift.monoid, npow_zero' := _, npow_succ' := _}
@[protected, instance]
Equations
- ulift.non_unital_comm_semiring = {add := has_add.add ulift.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul ulift.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul ulift.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}
@[protected, instance]
Equations
- ulift.comm_semiring = {add := has_add.add ulift.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul ulift.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul ulift.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast ulift.semiring, nat_cast_zero := _, nat_cast_succ := _, npow := monoid.npow ulift.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, instance]
Equations
- ulift.non_unital_non_assoc_ring = {add := has_add.add ulift.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul ulift.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg ulift.has_neg, sub := has_sub.sub ulift.has_sub, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul ulift.sub_neg_add_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul ulift.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
@[protected, instance]
Equations
- ulift.non_unital_ring = {add := has_add.add ulift.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul ulift.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg ulift.has_neg, sub := has_sub.sub ulift.has_sub, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul ulift.sub_neg_add_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul ulift.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
@[protected, instance]
Equations
- ulift.non_assoc_ring = {add := has_add.add ulift.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul ulift.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg ulift.has_neg, sub := has_sub.sub ulift.has_sub, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul ulift.sub_neg_add_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul ulift.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := 1, one_mul := _, mul_one := _, nat_cast := add_group_with_one.nat_cast ulift.add_group_with_one, nat_cast_zero := _, nat_cast_succ := _, int_cast := add_group_with_one.int_cast ulift.add_group_with_one, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}
@[protected, instance]
Equations
- ulift.ring = {add := has_add.add ulift.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul ulift.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg ulift.has_neg, sub := has_sub.sub ulift.has_sub, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul ulift.sub_neg_add_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_group_with_one.int_cast ulift.add_group_with_one, nat_cast := semiring.nat_cast ulift.semiring, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul ulift.has_mul, mul_assoc := _, one_mul := _, mul_one := _, npow := monoid.npow ulift.monoid, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
@[protected, instance]
Equations
- ulift.non_unital_comm_ring = {add := has_add.add ulift.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul ulift.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg ulift.has_neg, sub := has_sub.sub ulift.has_sub, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul ulift.sub_neg_add_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul ulift.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}
@[protected, instance]
Equations
- ulift.comm_ring = {add := ring.add ulift.ring, add_assoc := _, zero := ring.zero ulift.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul ulift.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg ulift.ring, sub := ring.sub ulift.ring, sub_eq_add_neg := _, zsmul := ring.zsmul ulift.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast ulift.ring, nat_cast := ring.nat_cast ulift.ring, one := ring.one ulift.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul ulift.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow ulift.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}