# Canonically ordered rings and semirings. #

## 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 multiplicative magma.

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

No zero divisors.

Instances
theorem CanonicallyOrderedCommSemiring.eq_zero_or_eq_zero_of_mul_eq_zero {α : Type u_2} [self : ] {a : α} {b : α} :
a * b = 0a = 0 b = 0

No zero divisors.

theorem Odd.pos {α : Type u} {a : α} [] :
Odd a0 < a
@[instance 100]
Equations
• =
@[instance 100]
instance CanonicallyOrderedCommSemiring.toCovariantClassMulLE {α : Type u} :
CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1
Equations
• =
@[instance 100]
Equations
• CanonicallyOrderedCommSemiring.toOrderedCommMonoid =
@[instance 100]
Equations
• CanonicallyOrderedCommSemiring.toOrderedCommSemiring = let __src := inst;
@[simp]
theorem CanonicallyOrderedCommSemiring.mul_pos {α : Type u} {a : α} {b : α} :
0 < a * b 0 < a 0 < b
theorem CanonicallyOrderedCommSemiring.mul_lt_mul_of_lt_of_lt {α : Type u} {a : α} {b : α} {c : α} {d : α} [] (hab : a < b) (hcd : c < d) :
a * c < b * d
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