mathlib documentation

algebra.ordered_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_cancel_add_comm_monoid {I : Type u} {f : I → Type v} [Π (i : I), ordered_cancel_add_comm_monoid (f i)] :
@[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)