Pi instances for ordered groups and monoids #
This file defines instances for ordered group, monoid, and related structures on Pi types.
@[protected, instance]
def
pi.ordered_comm_monoid
{ι : Type u_1}
{Z : ι → Type u_2}
[Π (i : ι), ordered_comm_monoid (Z i)] :
ordered_comm_monoid (Π (i : ι), Z i)
The product of a family of ordered commutative monoids is an ordered commutative monoid.
Equations
- pi.ordered_comm_monoid = {mul := comm_monoid.mul pi.comm_monoid, mul_assoc := _, one := comm_monoid.one pi.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow pi.comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le pi.partial_order, lt := partial_order.lt pi.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}
@[protected, instance]
def
pi.ordered_add_comm_monoid
{ι : Type u_1}
{Z : ι → Type u_2}
[Π (i : ι), ordered_add_comm_monoid (Z i)] :
ordered_add_comm_monoid (Π (i : ι), Z i)
The product of a family of ordered additive commutative monoids is an ordered additive commutative monoid.
Equations
- pi.ordered_add_comm_monoid = {add := add_comm_monoid.add pi.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero pi.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul pi.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le pi.partial_order, lt := partial_order.lt pi.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}
@[protected, instance]
def
pi.canonically_ordered_monoid
{ι : Type u_1}
{Z : ι → Type u_2}
[Π (i : ι), canonically_ordered_monoid (Z i)] :
canonically_ordered_monoid (Π (i : ι), Z i)
The product of a family of canonically ordered monoids is a canonically ordered monoid.
Equations
- pi.canonically_ordered_monoid = {mul := ordered_comm_monoid.mul pi.ordered_comm_monoid, mul_assoc := _, one := ordered_comm_monoid.one pi.ordered_comm_monoid, one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow pi.ordered_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := ordered_comm_monoid.le pi.ordered_comm_monoid, lt := ordered_comm_monoid.lt pi.ordered_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, bot := order_bot.bot pi.order_bot, bot_le := _, le_iff_exists_mul := _}
@[protected, instance]
def
pi.canonically_ordered_add_monoid
{ι : Type u_1}
{Z : ι → Type u_2}
[Π (i : ι), canonically_ordered_add_monoid (Z i)] :
canonically_ordered_add_monoid (Π (i : ι), Z i)
The product of a family of canonically ordered additive monoids is a canonically ordered additive monoid.
Equations
- pi.canonically_ordered_add_monoid = {add := ordered_add_comm_monoid.add pi.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero pi.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul pi.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_add_comm_monoid.le pi.ordered_add_comm_monoid, lt := ordered_add_comm_monoid.lt pi.ordered_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, bot := order_bot.bot pi.order_bot, bot_le := _, le_iff_exists_add := _}
@[protected, instance]
def
pi.ordered_cancel_add_comm_monoid
{I : Type u}
{f : I → Type v}
[Π (i : I), ordered_cancel_add_comm_monoid (f i)] :
ordered_cancel_add_comm_monoid (Π (i : I), f i)
Equations
- pi.ordered_cancel_add_comm_monoid = {add := has_add.add pi.has_add, add_assoc := _, add_left_cancel := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul pi.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := has_le.le pi.has_le, lt := has_lt.lt (preorder.to_has_lt (Π (i : I), f i)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}
@[protected, instance]
def
pi.ordered_cancel_comm_monoid
{I : Type u}
{f : I → Type v}
[Π (i : I), ordered_cancel_comm_monoid (f i)] :
ordered_cancel_comm_monoid (Π (i : I), f i)
Equations
- pi.ordered_cancel_comm_monoid = {mul := has_mul.mul pi.has_mul, mul_assoc := _, mul_left_cancel := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := has_le.le pi.has_le, lt := has_lt.lt (preorder.to_has_lt (Π (i : I), f i)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}
@[protected, instance]
def
pi.ordered_comm_group
{I : Type u}
{f : I → Type v}
[Π (i : I), ordered_comm_group (f i)] :
ordered_comm_group (Π (i : I), f i)
Equations
- pi.ordered_comm_group = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _, inv := comm_group.inv pi.comm_group, div := comm_group.div pi.comm_group, div_eq_mul_inv := _, zpow := comm_group.zpow pi.comm_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := has_le.le pi.has_le, lt := has_lt.lt (preorder.to_has_lt (Π (i : I), f i)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}
@[protected, instance]
def
pi.ordered_add_comm_group
{I : Type u}
{f : I → Type v}
[Π (i : I), ordered_add_comm_group (f i)] :
ordered_add_comm_group (Π (i : I), f i)
Equations
- pi.ordered_add_comm_group = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul pi.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg pi.add_comm_group, sub := add_comm_group.sub pi.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul pi.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := has_le.le pi.has_le, lt := has_lt.lt (preorder.to_has_lt (Π (i : I), f i)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}