algebra.order.pi

# 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
@[protected, instance]
def pi.ordered_add_comm_monoid {ι : Type u_1} {Z : ι Type u_2} [Π (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
@[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 : ι), ] :

The product of a family of canonically ordered monoids is a canonically ordered monoid.

Equations
@[protected, instance]
def pi.canonically_ordered_add_monoid {ι : Type u_1} {Z : ι Type u_2} [Π (i : ι), ] :

The product of a family of canonically ordered additive monoids is a canonically ordered additive monoid.

Equations
@[protected, instance]
def pi.ordered_cancel_add_comm_monoid {I : Type u} {f : I Type v} [Π (i : I), ] :
Equations
@[protected, instance]
def pi.ordered_cancel_comm_monoid {I : Type u} {f : I Type v} [Π (i : I), ] :
Equations
@[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
@[protected, instance]
def pi.ordered_add_comm_group {I : Type u} {f : I Type v} [Π (i : I), ] :
ordered_add_comm_group (Π (i : I), f i)
Equations
@[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
@[protected, instance]
def pi.ordered_comm_semiring {I : Type u} {f : I Type v} [Π (i : I), ] :
ordered_comm_semiring (Π (i : I), f i)
Equations
@[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
@[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
theorem function.const_nonneg_of_nonneg {α : Type u_2} (β : Type u_3) [has_zero α] [preorder α] {a : α} (ha : 0 a) :
0
theorem function.one_le_const_of_one_le {α : Type u_2} (β : Type u_3) [has_one α] [preorder α] {a : α} (ha : 1 a) :
1
theorem function.const_le_one_of_le_one {α : Type u_2} (β : Type u_3) [has_one α] [preorder α] {a : α} (ha : a 1) :
1
theorem function.const_nonpos_of_nonpos {α : Type u_2} (β : Type u_3) [has_zero α] [preorder α] {a : α} (ha : a 0) :
0
@[simp]
theorem function.one_le_const {α : Type u_2} {β : Type u_3} [has_one α] [preorder α] {a : α} [nonempty β] :
1 1 a
@[simp]
theorem function.const_nonneg {α : Type u_2} {β : Type u_3} [has_zero α] [preorder α] {a : α} [nonempty β] :
0 0 a
@[simp]
theorem function.const_pos {α : Type u_2} {β : Type u_3} [has_zero α] [preorder α] {a : α} [nonempty β] :
0 < 0 < a
@[simp]
theorem function.one_lt_const {α : Type u_2} {β : Type u_3} [has_one α] [preorder α] {a : α} [nonempty β] :
1 < 1 < a
@[simp]
theorem function.const_le_one {α : Type u_2} {β : Type u_3} [has_one α] [preorder α] {a : α} [nonempty β] :
1 a 1
@[simp]
theorem function.const_nonpos {α : Type u_2} {β : Type u_3} [has_zero α] [preorder α] {a : α} [nonempty β] :
0 a 0
@[simp]
theorem function.const_lt_one {α : Type u_2} {β : Type u_3} [has_one α] [preorder α] {a : α} [nonempty β] :
< 1 a < 1
@[simp]
theorem function.const_neg {α : Type u_2} {β : Type u_3} [has_zero α] [preorder α] {a : α} [nonempty β] :
< 0 a < 0

Extension for the positivity tactic: function.const is positive/nonnegative/nonzero if its input is.