# mathlib3documentation

algebra.order.ring.canonical

# Canoncially ordered rings and semirings. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

• canonically_ordered_comm_semiring
• canonically_ordered_add_monoid & multiplication & * respects ≤ & no zero divisors
• comm_semiring & a ≤ b ↔ ∃ c, b = a + c & no zero divisors

## TODO #

We're still missing some typeclasses, like

• canonically_ordered_semiring They have yet to come up in practice.
@[class]
structure canonically_ordered_comm_semiring (α : Type u_2) :
Type u_2
• add : α α α
• add_assoc : (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : (a : α), 0 + a = a
• add_zero : (a : α), a + 0 = a
• nsmul : α α
• nsmul_zero' : ( (x : α), . "try_refl_tac"
• nsmul_succ' : ( (n : ) (x : α), . "try_refl_tac"
• add_comm : (a b : α), a + b = b + a
• le : α α Prop
• lt : α α Prop
• le_refl : (a : α), a a
• le_trans : (a b c : α), a b b c a c
• lt_iff_le_not_le : ( (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : (a b : α), a b b a a = b
• add_le_add_left : (a b : α), a b (c : α), c + a c + b
• bot : α
• bot_le : (x : α), x
• exists_add_of_le : {a b : α}, a b ( (c : α), b = a + c)
• le_self_add : (a b : α), a a + b
• mul : α α α
• left_distrib : (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : (a : α), 0 * a = 0
• mul_zero : (a : α), a * 0 = 0
• mul_assoc : (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : (a : α), 1 * a = a
• mul_one : (a : α), a * 1 = a
• nat_cast : α
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : . "control_laws_tac"
• npow : α α
• npow_zero' : ( (x : α), . "try_refl_tac"
• npow_succ' : ( (n : ) (x : α), . "try_refl_tac"
• mul_comm : (a b : α), a * b = b * a
• eq_zero_or_eq_zero_of_mul_eq_zero : {a b : α}, a * b = 0 a = 0 b = 0

A canonically ordered commutative semiring is an ordered, commutative semiring in which a ≤ b iff there exists c with b = a + c. This is satisfied by the natural numbers, for example, but not the integers or other ordered groups.

Instances of this typeclass
Instances of other typeclasses for canonically_ordered_comm_semiring
• canonically_ordered_comm_semiring.has_sizeof_inst
@[instance]
theorem mul_add_mul_le_mul_add_mul {α : Type u} {a b c d : α} (hab : a b) (hcd : c d) :
a * d + b * c a * c + b * d

Binary rearrangement inequality.

theorem mul_add_mul_le_mul_add_mul' {α : Type u} {a b c d : α} (hba : b a) (hdc : d c) :
a d + b c a c + b d

Binary rearrangement inequality.

theorem mul_add_mul_lt_mul_add_mul {α : Type u} {a b c d : α} (hab : a < b) (hcd : c < d) :
a * d + b * c < a * c + b * d

Binary strict rearrangement inequality.

theorem mul_add_mul_lt_mul_add_mul' {α : Type u} {a b c d : α} (hba : b < a) (hdc : d < c) :
a d + b c < a c + b d

Binary rearrangement inequality.

@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem canonically_ordered_comm_semiring.mul_pos {α : Type u} {a b : α} :
0 < a * b 0 < a 0 < b
@[protected]
theorem add_le_cancellable.mul_tsub {α : Type u} {a b c : α} [has_sub α] (h : add_le_cancellable (a * c)) :
a * (b - c) = a * b - a * c
@[protected]
theorem add_le_cancellable.tsub_mul {α : Type u} {a b c : α} [has_sub α] (h : add_le_cancellable (b * c)) :
(a - b) * c = a * c - b * c
theorem mul_tsub {α : Type u} [has_sub α] (a b c : α) :
a * (b - c) = a * b - a * c
theorem tsub_mul {α : Type u} [has_sub α] (a b c : α) :
(a - b) * c = a * c - b * c