mathlib documentation

algebra.order.pi

Pi instances for ordered groups and monoids #

This file defines instances for ordered group, monoid, and related structures on Pi types.

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

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

Equations
@[instance]
def pi.ordered_cancel_add_comm_monoid {I : Type u} {f : I → Type v} [Π (i : I), ordered_cancel_add_comm_monoid (f i)] :
Equations
@[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
@[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
@[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