# Documentation

Mathlib.Algebra.Order.Ring.Canonical

# Canonically ordered rings and semirings. #

• CanonicallyOrderedCommSemiring
• CanonicallyOrderedAddCommMonoid & multiplication & * respects ≤ & no zero divisors
• CommSemiring & a ≤ b ↔ ∃ c, b = a + c & no zero divisors

## TODO #

We're still missing some typeclasses, like

• CanonicallyOrderedSemiring They have yet to come up in practice.
class CanonicallyOrderedCommSemiring (α : Type u_2) extends , , , :
Type u_2

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.

• 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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x +
• add_comm : ∀ (a b : α), a + b = b + a
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• bot : α
• bot_le : ∀ (a : α), a
• 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

Multiplication is left distributive over addition

• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c

Multiplication is right distributive over addition

• zero_mul : ∀ (a : α), 0 * a = 0

Zero is a left absorbing element for multiplication

• mul_zero : ∀ (a : α), a * 0 = 0

Zero is a right absorbing element for multiplication

• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)

Multiplication is associative

• one : α
• one_mul : ∀ (a : α), 1 * a = a

One is a left neutral element for multiplication

• mul_one : ∀ (a : α), a * 1 = a

One is a right neutral element for multiplication

• natCast : α
• natCast_zero :

The canonical map ℕ → R sends 0 : ℕ to 0 : R.

• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =

The canonical map ℕ → R is a homomorphism.

• npow : αα

Raising to the power of a natural number.

• npow_zero : ∀ (x : α),

Raising to the power (0 : ℕ) gives 1.

• npow_succ : ∀ (n : ) (x : α),

Raising to the power (n + 1 : ℕ) behaves as expected.

• mul_comm : ∀ (a b : α), a * b = b * a

Multiplication is commutative in a commutative semigroup.

• eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : α}, a * b = 0a = 0 b = 0

No zero divisors.

Instances
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.

Equations
• (_ : ) = (_ : )
instance CanonicallyOrderedCommSemiring.toCovariantClassMulLE {α : Type u} :
CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1
Equations
Equations
Equations
• CanonicallyOrderedCommSemiring.toOrderedCommSemiring = let src := inst; OrderedCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)
@[simp]
theorem CanonicallyOrderedCommSemiring.mul_pos {α : Type u} {a : α} {b : α} :
0 < a * b 0 < a 0 < b
theorem AddLECancellable.mul_tsub {α : Type u} {a : α} {b : α} {c : α} [Sub α] [] [IsTotal α fun (x x_1 : α) => x x_1] (h : AddLECancellable (a * c)) :
a * (b - c) = a * b - a * c
theorem AddLECancellable.tsub_mul {α : Type u} {a : α} {b : α} {c : α} [Sub α] [] [IsTotal α fun (x x_1 : α) => x x_1] (h : AddLECancellable (b * c)) :
(a - b) * c = a * c - b * c
theorem mul_tsub {α : Type u} [Sub α] [] [IsTotal α fun (x x_1 : α) => x x_1] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
a * (b - c) = a * b - a * c
theorem tsub_mul {α : Type u} [Sub α] [] [IsTotal α fun (x x_1 : α) => x x_1] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
(a - b) * c = a * c - b * c