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]
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 := _}
@[protected, instance]
@[protected, instance]
Equations
- ulift.field = {add := comm_ring.add ulift.comm_ring, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul ulift.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg ulift.comm_ring, sub := comm_ring.sub ulift.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul ulift.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast ulift.comm_ring, nat_cast := comm_ring.nat_cast ulift.comm_ring, one := comm_ring.one ulift.comm_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_ring.mul ulift.comm_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow ulift.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := has_inv.inv ulift.has_inv, div := has_div.div ulift.has_div, div_eq_mul_inv := _, zpow := λ (n : ℤ) (a : ulift α), {down := a.down ^ n}, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := coe coe_to_lift, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := has_smul.smul ulift.has_smul, qsmul_eq_mul' := _}