Pi instances for ordered groups and monoids #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.has_exists_add_of_le
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), has_le (α i)]
[Π (i : ι), has_add (α i)]
[∀ (i : ι), has_exists_add_of_le (α i)] :
has_exists_add_of_le (Π (i : ι), α i)
@[protected, instance]
def
pi.has_exists_mul_of_le
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), has_le (α i)]
[Π (i : ι), has_mul (α i)]
[∀ (i : ι), has_exists_mul_of_le (α i)] :
has_exists_mul_of_le (Π (i : ι), α i)
@[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 := _, exists_mul_of_le := _, le_self_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 := _, exists_add_of_le := _, le_self_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 := _, 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 := _, 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 := _}
@[protected, instance]
def
pi.ordered_semiring
{I : Type u}
{f : I → Type v}
[Π (i : I), ordered_semiring (f i)] :
ordered_semiring (Π (i : I), f i)
Equations
- pi.ordered_semiring = {add := semiring.add pi.semiring, add_assoc := _, zero := semiring.zero pi.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul pi.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul pi.semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one pi.semiring, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast pi.semiring, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow pi.semiring, npow_zero' := _, npow_succ' := _, 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 := _, zero_le_one := _, mul_le_mul_of_nonneg_left := _, mul_le_mul_of_nonneg_right := _}
@[protected, instance]
def
pi.ordered_comm_semiring
{I : Type u}
{f : I → Type v}
[Π (i : I), ordered_comm_semiring (f i)] :
ordered_comm_semiring (Π (i : I), f i)
Equations
- pi.ordered_comm_semiring = {add := comm_semiring.add pi.comm_semiring, add_assoc := _, zero := comm_semiring.zero pi.comm_semiring, zero_add := _, add_zero := _, nsmul := comm_semiring.nsmul pi.comm_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_semiring.mul pi.comm_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := comm_semiring.one pi.comm_semiring, one_mul := _, mul_one := _, nat_cast := comm_semiring.nat_cast pi.comm_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := comm_semiring.npow pi.comm_semiring, npow_zero' := _, npow_succ' := _, le := ordered_semiring.le pi.ordered_semiring, lt := ordered_semiring.lt pi.ordered_semiring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_le_mul_of_nonneg_left := _, mul_le_mul_of_nonneg_right := _, mul_comm := _}
@[protected, instance]
def
pi.ordered_ring
{I : Type u}
{f : I → Type v}
[Π (i : I), ordered_ring (f i)] :
ordered_ring (Π (i : I), f i)
Equations
- pi.ordered_ring = {add := ring.add pi.ring, add_assoc := _, zero := ring.zero pi.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul pi.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg pi.ring, sub := ring.sub pi.ring, sub_eq_add_neg := _, zsmul := ring.zsmul pi.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast pi.ring, nat_cast := ring.nat_cast pi.ring, one := ring.one pi.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul pi.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow pi.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := ordered_semiring.le pi.ordered_semiring, lt := ordered_semiring.lt pi.ordered_semiring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_nonneg := _}
@[protected, instance]
def
pi.ordered_comm_ring
{I : Type u}
{f : I → Type v}
[Π (i : I), ordered_comm_ring (f i)] :
ordered_comm_ring (Π (i : I), f i)
Equations
- pi.ordered_comm_ring = {add := comm_ring.add pi.comm_ring, add_assoc := _, zero := comm_ring.zero pi.comm_ring, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul pi.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg pi.comm_ring, sub := comm_ring.sub pi.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul pi.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast pi.comm_ring, nat_cast := comm_ring.nat_cast pi.comm_ring, one := comm_ring.one pi.comm_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_ring.mul pi.comm_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow pi.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := ordered_ring.le pi.ordered_ring, lt := ordered_ring.lt pi.ordered_ring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_nonneg := _, mul_comm := _}
theorem
function.const_nonneg_of_nonneg
{α : Type u_2}
(β : Type u_3)
[has_zero α]
[preorder α]
{a : α}
(ha : 0 ≤ a) :
0 ≤ function.const β a
theorem
function.one_le_const_of_one_le
{α : Type u_2}
(β : Type u_3)
[has_one α]
[preorder α]
{a : α}
(ha : 1 ≤ a) :
1 ≤ function.const β a
theorem
function.const_le_one_of_le_one
{α : Type u_2}
(β : Type u_3)
[has_one α]
[preorder α]
{a : α}
(ha : a ≤ 1) :
function.const β a ≤ 1
theorem
function.const_nonpos_of_nonpos
{α : Type u_2}
(β : Type u_3)
[has_zero α]
[preorder α]
{a : α}
(ha : a ≤ 0) :
function.const β a ≤ 0