mathlib documentation


Pi instances for ordered groups and monoids #

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

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