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).
@[instance]
Equations
- ulift.has_one = {one := {down := 1}}
@[instance]
@[instance]
Equations
- ulift.semigroup = {mul := has_mul.mul ulift.has_mul, mul_assoc := _}
The additive equivalence between ulift α and α.
The multiplicative equivalence between ulift α and α.
Equations
- ulift.mul_equiv = {to_fun := ulift.down α, inv_fun := ulift.up α, left_inv := _, right_inv := _, map_mul' := _}
@[instance]
Equations
- ulift.comm_semigroup = {mul := has_mul.mul ulift.has_mul, mul_assoc := _, mul_comm := _}
@[instance]
@[instance]
Equations
- ulift.monoid = {mul := has_mul.mul ulift.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _}
@[instance]
Equations
- ulift.comm_monoid = {mul := has_mul.mul ulift.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, mul_comm := _}
@[instance]
@[instance]
Equations
- ulift.group = {mul := has_mul.mul ulift.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, inv := has_inv.inv ulift.has_inv, mul_left_inv := _}
@[instance]
Equations
- ulift.comm_group = {mul := has_mul.mul ulift.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, inv := has_inv.inv ulift.has_inv, mul_left_inv := _, mul_comm := _}
@[instance]
@[instance]
Equations
- ulift.left_cancel_semigroup = {mul := has_mul.mul ulift.has_mul, mul_assoc := _, mul_left_cancel := _}
@[instance]
@[instance]
Equations
- ulift.right_cancel_semigroup = {mul := has_mul.mul ulift.has_mul, mul_assoc := _, mul_right_cancel := _}
@[instance]