Pi instances for ordered groups and monoids #
This file defines instances for ordered group, monoid, and related structures on Pi types.
@[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)
@[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 := _, mul_left_cancel := _, one := 1, one_mul := _, mul_one := _, npow := λ (n : ℕ) (x : Π (i : I), f i) (i : I), npow n (x i), npow_zero' := _, npow_succ' := _, mul_comm := _, le := has_le.le (preorder.to_has_le (Π (i : I), f i)), 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 := λ (n : ℕ) (x : Π (i : I), f i) (i : I), npow n (x i), npow_zero' := _, npow_succ' := _, inv := comm_group.inv pi.comm_group, div := comm_group.div pi.comm_group, div_eq_mul_inv := _, gpow := comm_group.gpow pi.comm_group, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_left_inv := _, mul_comm := _, le := has_le.le (preorder.to_has_le (Π (i : I), f i)), 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)