Ordered monoid structures on multiplicative α
and additive α
. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
- multiplicative.ordered_comm_monoid = {mul := comm_monoid.mul multiplicative.comm_monoid, mul_assoc := _, one := comm_monoid.one multiplicative.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow multiplicative.comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le multiplicative.partial_order, lt := partial_order.lt multiplicative.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}
@[protected, instance]
Equations
- additive.ordered_add_comm_monoid = {add := add_comm_monoid.add additive.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero additive.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul additive.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le additive.partial_order, lt := partial_order.lt additive.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}
@[protected, instance]
Equations
- multiplicative.ordered_cancel_comm_monoid = {mul := ordered_comm_monoid.mul multiplicative.ordered_comm_monoid, mul_assoc := _, one := ordered_comm_monoid.one multiplicative.ordered_comm_monoid, one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow multiplicative.ordered_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := ordered_comm_monoid.le multiplicative.ordered_comm_monoid, lt := ordered_comm_monoid.lt multiplicative.ordered_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}
@[protected, instance]
Equations
- additive.ordered_cancel_add_comm_monoid = {add := ordered_add_comm_monoid.add additive.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero additive.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul additive.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_add_comm_monoid.le additive.ordered_add_comm_monoid, lt := ordered_add_comm_monoid.lt additive.ordered_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}
@[protected, instance]
Equations
- multiplicative.linear_ordered_comm_monoid = {le := linear_order.le multiplicative.linear_order, lt := linear_order.lt multiplicative.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le multiplicative.linear_order, decidable_eq := linear_order.decidable_eq multiplicative.linear_order, decidable_lt := linear_order.decidable_lt multiplicative.linear_order, max := linear_order.max multiplicative.linear_order, max_def := _, min := linear_order.min multiplicative.linear_order, min_def := _, mul := ordered_comm_monoid.mul multiplicative.ordered_comm_monoid, mul_assoc := _, one := ordered_comm_monoid.one multiplicative.ordered_comm_monoid, one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow multiplicative.ordered_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_mul_left := _}
@[protected, instance]
Equations
- additive.linear_ordered_add_comm_monoid = {le := linear_order.le additive.linear_order, lt := linear_order.lt additive.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le additive.linear_order, decidable_eq := linear_order.decidable_eq additive.linear_order, decidable_lt := linear_order.decidable_lt additive.linear_order, max := linear_order.max additive.linear_order, max_def := _, min := linear_order.min additive.linear_order, min_def := _, add := ordered_add_comm_monoid.add additive.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero additive.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul additive.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, add_le_add_left := _}
@[protected, instance]
def
multiplicative.has_exists_mul_of_le
{α : Type u}
[has_add α]
[has_le α]
[has_exists_add_of_le α] :
@[protected, instance]
@[protected, instance]
Equations
- multiplicative.canonically_ordered_monoid = {mul := ordered_comm_monoid.mul multiplicative.ordered_comm_monoid, mul_assoc := _, one := ordered_comm_monoid.one multiplicative.ordered_comm_monoid, one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow multiplicative.ordered_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := ordered_comm_monoid.le multiplicative.ordered_comm_monoid, lt := ordered_comm_monoid.lt multiplicative.ordered_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, bot := order_bot.bot multiplicative.order_bot, bot_le := _, exists_mul_of_le := _, le_self_mul := _}
@[protected, instance]
Equations
- additive.canonically_ordered_add_monoid = {add := ordered_add_comm_monoid.add additive.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero additive.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul additive.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_add_comm_monoid.le additive.ordered_add_comm_monoid, lt := ordered_add_comm_monoid.lt additive.ordered_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, bot := order_bot.bot additive.order_bot, bot_le := _, exists_add_of_le := _, le_self_add := _}
@[protected, instance]
def
multiplicative.canonically_linear_ordered_monoid
{α : Type u}
[canonically_linear_ordered_add_monoid α] :
Equations
- multiplicative.canonically_linear_ordered_monoid = {mul := canonically_ordered_monoid.mul multiplicative.canonically_ordered_monoid, mul_assoc := _, one := canonically_ordered_monoid.one multiplicative.canonically_ordered_monoid, one_mul := _, mul_one := _, npow := canonically_ordered_monoid.npow multiplicative.canonically_ordered_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := canonically_ordered_monoid.le multiplicative.canonically_ordered_monoid, lt := canonically_ordered_monoid.lt multiplicative.canonically_ordered_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, bot := canonically_ordered_monoid.bot multiplicative.canonically_ordered_monoid, bot_le := _, exists_mul_of_le := _, le_self_mul := _, le_total := _, decidable_le := linear_order.decidable_le multiplicative.linear_order, decidable_eq := linear_order.decidable_eq multiplicative.linear_order, decidable_lt := linear_order.decidable_lt multiplicative.linear_order, max := linear_order.max multiplicative.linear_order, max_def := _, min := linear_order.min multiplicative.linear_order, min_def := _}
@[protected, instance]
def
additive.canonically_linear_ordered_add_monoid
{α : Type u}
[canonically_linear_ordered_monoid α] :
Equations
- additive.canonically_linear_ordered_add_monoid = {add := canonically_ordered_add_monoid.add additive.canonically_ordered_add_monoid, add_assoc := _, zero := canonically_ordered_add_monoid.zero additive.canonically_ordered_add_monoid, zero_add := _, add_zero := _, nsmul := canonically_ordered_add_monoid.nsmul additive.canonically_ordered_add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := canonically_ordered_add_monoid.le additive.canonically_ordered_add_monoid, lt := canonically_ordered_add_monoid.lt additive.canonically_ordered_add_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, bot := canonically_ordered_add_monoid.bot additive.canonically_ordered_add_monoid, bot_le := _, exists_add_of_le := _, le_self_add := _, le_total := _, decidable_le := linear_order.decidable_le additive.linear_order, decidable_eq := linear_order.decidable_eq additive.linear_order, decidable_lt := linear_order.decidable_lt additive.linear_order, max := linear_order.max additive.linear_order, max_def := _, min := linear_order.min additive.linear_order, min_def := _}
@[simp]
theorem
additive.of_mul_le
{α : Type u}
[preorder α]
{a b : α} :
⇑additive.of_mul a ≤ ⇑additive.of_mul b ↔ a ≤ b
@[simp]
theorem
additive.of_mul_lt
{α : Type u}
[preorder α]
{a b : α} :
⇑additive.of_mul a < ⇑additive.of_mul b ↔ a < b
@[simp]
theorem
additive.to_mul_le
{α : Type u}
[preorder α]
{a b : additive α} :
⇑additive.to_mul a ≤ ⇑additive.to_mul b ↔ a ≤ b
@[simp]
theorem
additive.to_mul_lt
{α : Type u}
[preorder α]
{a b : additive α} :
⇑additive.to_mul a < ⇑additive.to_mul b ↔ a < b
@[simp]
theorem
multiplicative.of_add_le
{α : Type u}
[preorder α]
{a b : α} :
⇑multiplicative.of_add a ≤ ⇑multiplicative.of_add b ↔ a ≤ b
@[simp]
theorem
multiplicative.of_add_lt
{α : Type u}
[preorder α]
{a b : α} :
⇑multiplicative.of_add a < ⇑multiplicative.of_add b ↔ a < b
@[simp]
theorem
multiplicative.to_add_le
{α : Type u}
[preorder α]
{a b : multiplicative α} :
⇑multiplicative.to_add a ≤ ⇑multiplicative.to_add b ↔ a ≤ b
@[simp]
theorem
multiplicative.to_add_lt
{α : Type u}
[preorder α]
{a b : multiplicative α} :
⇑multiplicative.to_add a < ⇑multiplicative.to_add b ↔ a < b