ulift
instances for groups and monoids #
This file defines instances for group, monoid, semigroup and related structures on ulift
types.
(Recall ulift α
is just a "copy" of a type α
in a higher universe.)
We use tactic.pi_instance_derive_field
, even though it wasn't intended for this purpose,
which seems to work fine.
We also provide ulift.mul_equiv : ulift R ≃* R
(and its additive analogue).
@[protected, instance]
Equations
- ulift.has_zero = {zero := {down := 0}}
@[protected, instance]
Equations
- ulift.has_one = {one := {down := 1}}
The additive equivalence between ulift α
and α
.
Equations
- add_equiv.ulift = {to_fun := equiv.ulift.to_fun, inv_fun := equiv.ulift.inv_fun, left_inv := _, right_inv := _, map_add' := _}
The multiplicative equivalence between ulift α
and α
.
Equations
- mul_equiv.ulift = {to_fun := equiv.ulift.to_fun, inv_fun := equiv.ulift.inv_fun, left_inv := _, right_inv := _, map_mul' := _}
@[protected, instance]
Equations
- ulift.add_semigroup = function.injective.add_semigroup ⇑add_equiv.ulift ulift.add_semigroup._proof_1 ulift.add_semigroup._proof_2
@[protected, instance]
Equations
- ulift.semigroup = function.injective.semigroup ⇑mul_equiv.ulift ulift.semigroup._proof_1 ulift.semigroup._proof_2
@[protected, instance]
Equations
- ulift.add_comm_semigroup = function.injective.add_comm_semigroup ⇑equiv.ulift ulift.add_comm_semigroup._proof_1 ulift.add_comm_semigroup._proof_2
@[protected, instance]
Equations
- ulift.comm_semigroup = function.injective.comm_semigroup ⇑equiv.ulift ulift.comm_semigroup._proof_1 ulift.comm_semigroup._proof_2
@[protected, instance]
Equations
- ulift.mul_one_class = function.injective.mul_one_class ⇑equiv.ulift ulift.mul_one_class._proof_1 ulift.mul_one_class._proof_2 ulift.mul_one_class._proof_3
@[protected, instance]
Equations
- ulift.add_zero_class = function.injective.add_zero_class ⇑equiv.ulift ulift.add_zero_class._proof_1 ulift.add_zero_class._proof_2 ulift.add_zero_class._proof_3
@[protected, instance]
@[protected, instance]
Equations
- ulift.add_monoid = function.injective.add_monoid_smul ⇑equiv.ulift ulift.add_monoid._proof_1 ulift.add_monoid._proof_2 ulift.add_monoid._proof_3 ulift.add_monoid._proof_4
@[protected, instance]
Equations
- ulift.monoid = function.injective.monoid_pow ⇑equiv.ulift ulift.monoid._proof_1 ulift.monoid._proof_2 ulift.monoid._proof_3 ulift.monoid._proof_4
@[protected, instance]
Equations
- ulift.add_comm_monoid = {add := add_monoid.add ulift.add_monoid, add_assoc := _, zero := add_monoid.zero ulift.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul ulift.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, instance]
Equations
- ulift.comm_monoid = {mul := monoid.mul ulift.monoid, mul_assoc := _, one := monoid.one ulift.monoid, one_mul := _, mul_one := _, npow := monoid.npow ulift.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, instance]
Equations
- ulift.div_inv_monoid = function.injective.div_inv_monoid_pow ⇑equiv.ulift ulift.div_inv_monoid._proof_1 ulift.div_inv_monoid._proof_2 ulift.div_inv_monoid._proof_3 ulift.div_inv_monoid._proof_4 ulift.div_inv_monoid._proof_5 ulift.div_inv_monoid._proof_6 ulift.div_inv_monoid._proof_7
@[protected, instance]
Equations
- ulift.sub_neg_add_monoid = function.injective.sub_neg_monoid_smul ⇑equiv.ulift ulift.sub_neg_add_monoid._proof_1 ulift.sub_neg_add_monoid._proof_2 ulift.sub_neg_add_monoid._proof_3 ulift.sub_neg_add_monoid._proof_4 ulift.sub_neg_add_monoid._proof_5 ulift.sub_neg_add_monoid._proof_6 ulift.sub_neg_add_monoid._proof_7
@[protected, instance]
Equations
- ulift.add_group = function.injective.add_group_smul ⇑equiv.ulift ulift.add_group._proof_1 ulift.add_group._proof_2 ulift.add_group._proof_3 ulift.add_group._proof_4 ulift.add_group._proof_5 ulift.add_group._proof_6 ulift.add_group._proof_7
@[protected, instance]
Equations
- ulift.group = function.injective.group_pow ⇑equiv.ulift ulift.group._proof_1 ulift.group._proof_2 ulift.group._proof_3 ulift.group._proof_4 ulift.group._proof_5 ulift.group._proof_6 ulift.group._proof_7
@[protected, instance]
Equations
- ulift.comm_group = {mul := group.mul ulift.group, mul_assoc := _, one := group.one ulift.group, one_mul := _, mul_one := _, npow := group.npow ulift.group, npow_zero' := _, npow_succ' := _, inv := group.inv ulift.group, div := group.div ulift.group, div_eq_mul_inv := _, zpow := group.zpow ulift.group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
@[protected, instance]
Equations
- ulift.add_comm_group = {add := add_group.add ulift.add_group, add_assoc := _, zero := add_group.zero ulift.add_group, zero_add := _, add_zero := _, nsmul := add_group.nsmul ulift.add_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg ulift.add_group, sub := add_group.sub ulift.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul ulift.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[protected, instance]
Equations
- ulift.add_left_cancel_semigroup = function.injective.add_left_cancel_semigroup ⇑equiv.ulift ulift.add_left_cancel_semigroup._proof_1 ulift.add_left_cancel_semigroup._proof_2
@[protected, instance]
Equations
- ulift.left_cancel_semigroup = function.injective.left_cancel_semigroup ⇑equiv.ulift ulift.left_cancel_semigroup._proof_1 ulift.left_cancel_semigroup._proof_2
@[protected, instance]
Equations
- ulift.right_cancel_semigroup = function.injective.right_cancel_semigroup ⇑equiv.ulift ulift.right_cancel_semigroup._proof_1 ulift.right_cancel_semigroup._proof_2
@[protected, instance]
Equations
- ulift.add_right_cancel_semigroup = function.injective.add_right_cancel_semigroup ⇑equiv.ulift ulift.add_right_cancel_semigroup._proof_1 ulift.add_right_cancel_semigroup._proof_2
@[protected, instance]
Equations
- ulift.left_cancel_monoid = {mul := monoid.mul ulift.monoid, mul_assoc := _, mul_left_cancel := _, one := monoid.one ulift.monoid, one_mul := _, mul_one := _, npow := monoid.npow ulift.monoid, npow_zero' := _, npow_succ' := _}
@[protected, instance]
Equations
- ulift.add_left_cancel_monoid = {add := add_monoid.add ulift.add_monoid, add_assoc := _, add_left_cancel := _, zero := add_monoid.zero ulift.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul ulift.add_monoid, nsmul_zero' := _, nsmul_succ' := _}
@[protected, instance]
Equations
- ulift.add_right_cancel_monoid = {add := add_monoid.add ulift.add_monoid, add_assoc := _, add_right_cancel := _, zero := add_monoid.zero ulift.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul ulift.add_monoid, nsmul_zero' := _, nsmul_succ' := _}
@[protected, instance]
Equations
- ulift.right_cancel_monoid = {mul := monoid.mul ulift.monoid, mul_assoc := _, mul_right_cancel := _, one := monoid.one ulift.monoid, one_mul := _, mul_one := _, npow := monoid.npow ulift.monoid, npow_zero' := _, npow_succ' := _}
@[protected, instance]
Equations
- ulift.cancel_monoid = {mul := left_cancel_monoid.mul ulift.left_cancel_monoid, mul_assoc := _, mul_left_cancel := _, one := left_cancel_monoid.one ulift.left_cancel_monoid, one_mul := _, mul_one := _, npow := left_cancel_monoid.npow ulift.left_cancel_monoid, npow_zero' := _, npow_succ' := _, mul_right_cancel := _}
@[protected, instance]
Equations
- ulift.add_cancel_monoid = {add := add_left_cancel_monoid.add ulift.add_left_cancel_monoid, add_assoc := _, add_left_cancel := _, zero := add_left_cancel_monoid.zero ulift.add_left_cancel_monoid, zero_add := _, add_zero := _, nsmul := add_left_cancel_monoid.nsmul ulift.add_left_cancel_monoid, nsmul_zero' := _, nsmul_succ' := _, add_right_cancel := _}
@[protected, instance]
Equations
- ulift.cancel_comm_monoid = {mul := cancel_monoid.mul ulift.cancel_monoid, mul_assoc := _, mul_left_cancel := _, one := cancel_monoid.one ulift.cancel_monoid, one_mul := _, mul_one := _, npow := cancel_monoid.npow ulift.cancel_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}