Products of ordered commutative groups. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, instance]
def
prod.ordered_comm_group
{G : Type u_2}
{H : Type u_3}
[ordered_comm_group G]
[ordered_comm_group H] :
ordered_comm_group (G × H)
Equations
- prod.ordered_comm_group = {mul := comm_group.mul prod.comm_group, mul_assoc := _, one := comm_group.one prod.comm_group, one_mul := _, mul_one := _, npow := comm_group.npow prod.comm_group, npow_zero' := _, npow_succ' := _, inv := comm_group.inv prod.comm_group, div := comm_group.div prod.comm_group, div_eq_mul_inv := _, zpow := comm_group.zpow prod.comm_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := partial_order.le (prod.partial_order G H), lt := partial_order.lt (prod.partial_order G H), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}
@[protected, instance]
def
prod.ordered_add_comm_group
{G : Type u_2}
{H : Type u_3}
[ordered_add_comm_group G]
[ordered_add_comm_group H] :
ordered_add_comm_group (G × H)
Equations
- prod.ordered_add_comm_group = {add := add_comm_group.add prod.add_comm_group, add_assoc := _, zero := add_comm_group.zero prod.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul prod.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg prod.add_comm_group, sub := add_comm_group.sub prod.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul prod.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := partial_order.le (prod.partial_order G H), lt := partial_order.lt (prod.partial_order G H), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}