mathlib3 documentation

algebra.order.group.instances

Additional instances for ordered commutative groups. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]

def order_dual.ordered_add_comm_group {α : Type u_1} [ordered_add_comm_group α] :

ordered_add_comm_group αᵒᵈ

Equations

order_dual.ordered_add_comm_group = {add := ordered_add_comm_monoid.add order_dual.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero order_dual.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul order_dual.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg order_dual.add_group, sub := add_group.sub order_dual.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul order_dual.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := ordered_add_comm_monoid.le order_dual.ordered_add_comm_monoid, lt := ordered_add_comm_monoid.lt order_dual.ordered_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}

@[protected, instance]

def order_dual.ordered_comm_group {α : Type u_1} [ordered_comm_group α] :

ordered_comm_group αᵒᵈ

Equations

order_dual.ordered_comm_group = {mul := ordered_comm_monoid.mul order_dual.ordered_comm_monoid, mul_assoc := _, one := ordered_comm_monoid.one order_dual.ordered_comm_monoid, one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow order_dual.ordered_comm_monoid, npow_zero' := _, npow_succ' := _, inv := group.inv order_dual.group, div := group.div order_dual.group, div_eq_mul_inv := _, zpow := group.zpow order_dual.group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := ordered_comm_monoid.le order_dual.ordered_comm_monoid, lt := ordered_comm_monoid.lt order_dual.ordered_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}

@[protected, instance]

def order_dual.linear_ordered_comm_group {α : Type u_1} [linear_ordered_comm_group α] :

linear_ordered_comm_group αᵒᵈ

Equations

order_dual.linear_ordered_comm_group = {mul := ordered_comm_group.mul order_dual.ordered_comm_group, mul_assoc := _, one := ordered_comm_group.one order_dual.ordered_comm_group, one_mul := _, mul_one := _, npow := ordered_comm_group.npow order_dual.ordered_comm_group, npow_zero' := _, npow_succ' := _, inv := ordered_comm_group.inv order_dual.ordered_comm_group, div := ordered_comm_group.div order_dual.ordered_comm_group, div_eq_mul_inv := _, zpow := ordered_comm_group.zpow order_dual.ordered_comm_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := ordered_comm_group.le order_dual.ordered_comm_group, lt := ordered_comm_group.lt order_dual.ordered_comm_group, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_total := _, decidable_le := linear_order.decidable_le (order_dual.linear_order α), decidable_eq := linear_order.decidable_eq (order_dual.linear_order α), decidable_lt := linear_order.decidable_lt (order_dual.linear_order α), max := linear_order.max (order_dual.linear_order α), max_def := _, min := linear_order.min (order_dual.linear_order α), min_def := _}

@[protected, instance]

def order_dual.linear_ordered_add_comm_group {α : Type u_1} [linear_ordered_add_comm_group α] :

linear_ordered_add_comm_group αᵒᵈ

Equations

order_dual.linear_ordered_add_comm_group = {add := ordered_add_comm_group.add order_dual.ordered_add_comm_group, add_assoc := _, zero := ordered_add_comm_group.zero order_dual.ordered_add_comm_group, zero_add := _, add_zero := _, nsmul := ordered_add_comm_group.nsmul order_dual.ordered_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := ordered_add_comm_group.neg order_dual.ordered_add_comm_group, sub := ordered_add_comm_group.sub order_dual.ordered_add_comm_group, sub_eq_add_neg := _, zsmul := ordered_add_comm_group.zsmul order_dual.ordered_add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := ordered_add_comm_group.le order_dual.ordered_add_comm_group, lt := ordered_add_comm_group.lt order_dual.ordered_add_comm_group, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_total := _, decidable_le := linear_order.decidable_le (order_dual.linear_order α), decidable_eq := linear_order.decidable_eq (order_dual.linear_order α), decidable_lt := linear_order.decidable_lt (order_dual.linear_order α), max := linear_order.max (order_dual.linear_order α), max_def := _, min := linear_order.min (order_dual.linear_order α), min_def := _}