Products of ordered monoids #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, instance]
def
prod.ordered_add_comm_monoid
{α : Type u_1}
{β : Type u_2}
[ordered_add_comm_monoid α]
[ordered_add_comm_monoid β] :
ordered_add_comm_monoid (α × β)
Equations
- prod.ordered_add_comm_monoid = {add := add_comm_monoid.add prod.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero prod.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul prod.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le (prod.partial_order α β), lt := partial_order.lt (prod.partial_order α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}
@[protected, instance]
def
prod.ordered_comm_monoid
{α : Type u_1}
{β : Type u_2}
[ordered_comm_monoid α]
[ordered_comm_monoid β] :
ordered_comm_monoid (α × β)
Equations
- prod.ordered_comm_monoid = {mul := comm_monoid.mul prod.comm_monoid, mul_assoc := _, one := comm_monoid.one prod.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow prod.comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le (prod.partial_order α β), lt := partial_order.lt (prod.partial_order α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}
@[protected, instance]
def
prod.ordered_cancel_comm_monoid
{M : Type u_3}
{N : Type u_4}
[ordered_cancel_comm_monoid M]
[ordered_cancel_comm_monoid N] :
ordered_cancel_comm_monoid (M × N)
Equations
- prod.ordered_cancel_comm_monoid = {mul := ordered_comm_monoid.mul prod.ordered_comm_monoid, mul_assoc := _, one := ordered_comm_monoid.one prod.ordered_comm_monoid, one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow prod.ordered_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := ordered_comm_monoid.le prod.ordered_comm_monoid, lt := ordered_comm_monoid.lt prod.ordered_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}
@[protected, instance]
def
prod.ordered_cancel_add_comm_monoid
{M : Type u_3}
{N : Type u_4}
[ordered_cancel_add_comm_monoid M]
[ordered_cancel_add_comm_monoid N] :
Equations
- prod.ordered_cancel_add_comm_monoid = {add := ordered_add_comm_monoid.add prod.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero prod.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul prod.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_add_comm_monoid.le prod.ordered_add_comm_monoid, lt := ordered_add_comm_monoid.lt prod.ordered_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}
@[protected, instance]
def
prod.has_exists_add_of_le
{α : Type u_1}
{β : Type u_2}
[has_le α]
[has_le β]
[has_add α]
[has_add β]
[has_exists_add_of_le α]
[has_exists_add_of_le β] :
has_exists_add_of_le (α × β)
@[protected, instance]
def
prod.has_exists_mul_of_le
{α : Type u_1}
{β : Type u_2}
[has_le α]
[has_le β]
[has_mul α]
[has_mul β]
[has_exists_mul_of_le α]
[has_exists_mul_of_le β] :
has_exists_mul_of_le (α × β)
@[protected, instance]
def
prod.canonically_ordered_add_monoid
{α : Type u_1}
{β : Type u_2}
[canonically_ordered_add_monoid α]
[canonically_ordered_add_monoid β] :
Equations
- prod.canonically_ordered_add_monoid = {add := ordered_add_comm_monoid.add prod.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero prod.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul prod.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_add_comm_monoid.le prod.ordered_add_comm_monoid, lt := ordered_add_comm_monoid.lt prod.ordered_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, bot := order_bot.bot (prod.order_bot α β), bot_le := _, exists_add_of_le := _, le_self_add := _}
@[protected, instance]
def
prod.canonically_ordered_monoid
{α : Type u_1}
{β : Type u_2}
[canonically_ordered_monoid α]
[canonically_ordered_monoid β] :
canonically_ordered_monoid (α × β)
Equations
- prod.canonically_ordered_monoid = {mul := ordered_comm_monoid.mul prod.ordered_comm_monoid, mul_assoc := _, one := ordered_comm_monoid.one prod.ordered_comm_monoid, one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow prod.ordered_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := ordered_comm_monoid.le prod.ordered_comm_monoid, lt := ordered_comm_monoid.lt prod.ordered_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, bot := order_bot.bot (prod.order_bot α β), bot_le := _, exists_mul_of_le := _, le_self_mul := _}