Ordered group structures on multiplicative α
and additive α
. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, instance]
Equations
- multiplicative.ordered_comm_group = {mul := comm_group.mul multiplicative.comm_group, mul_assoc := _, one := comm_group.one multiplicative.comm_group, one_mul := _, mul_one := _, npow := comm_group.npow multiplicative.comm_group, npow_zero' := _, npow_succ' := _, inv := comm_group.inv multiplicative.comm_group, div := comm_group.div multiplicative.comm_group, div_eq_mul_inv := _, zpow := comm_group.zpow multiplicative.comm_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := ordered_comm_monoid.le multiplicative.ordered_comm_monoid, lt := ordered_comm_monoid.lt multiplicative.ordered_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}
@[protected, instance]
Equations
- additive.ordered_add_comm_group = {add := add_comm_group.add additive.add_comm_group, add_assoc := _, zero := add_comm_group.zero additive.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul additive.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg additive.add_comm_group, sub := add_comm_group.sub additive.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul additive.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := ordered_add_comm_monoid.le additive.ordered_add_comm_monoid, lt := ordered_add_comm_monoid.lt additive.ordered_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}
@[protected, instance]
Equations
- multiplicative.linear_ordered_comm_group = {mul := ordered_comm_group.mul multiplicative.ordered_comm_group, mul_assoc := _, one := ordered_comm_group.one multiplicative.ordered_comm_group, one_mul := _, mul_one := _, npow := ordered_comm_group.npow multiplicative.ordered_comm_group, npow_zero' := _, npow_succ' := _, inv := ordered_comm_group.inv multiplicative.ordered_comm_group, div := ordered_comm_group.div multiplicative.ordered_comm_group, div_eq_mul_inv := _, zpow := ordered_comm_group.zpow multiplicative.ordered_comm_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := linear_order.le multiplicative.linear_order, lt := linear_order.lt multiplicative.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_total := _, decidable_le := linear_order.decidable_le multiplicative.linear_order, decidable_eq := linear_order.decidable_eq multiplicative.linear_order, decidable_lt := linear_order.decidable_lt multiplicative.linear_order, max := linear_order.max multiplicative.linear_order, max_def := _, min := linear_order.min multiplicative.linear_order, min_def := _}
@[protected, instance]
Equations
- additive.linear_ordered_add_comm_group = {add := ordered_add_comm_group.add additive.ordered_add_comm_group, add_assoc := _, zero := ordered_add_comm_group.zero additive.ordered_add_comm_group, zero_add := _, add_zero := _, nsmul := ordered_add_comm_group.nsmul additive.ordered_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := ordered_add_comm_group.neg additive.ordered_add_comm_group, sub := ordered_add_comm_group.sub additive.ordered_add_comm_group, sub_eq_add_neg := _, zsmul := ordered_add_comm_group.zsmul additive.ordered_add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := linear_order.le additive.linear_order, lt := linear_order.lt additive.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_total := _, decidable_le := linear_order.decidable_le additive.linear_order, decidable_eq := linear_order.decidable_eq additive.linear_order, decidable_lt := linear_order.decidable_lt additive.linear_order, max := linear_order.max additive.linear_order, max_def := _, min := linear_order.min additive.linear_order, min_def := _}