Canoncially ordered rings and semirings.

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

TODO

We're still missing some typeclasses, like

• CanonicallyOrderedSemiring They have yet to come up in practice.

ink

class CanonicallyOrderedCommSemiring (α : Type u_1) extends CanonicallyOrderedAddMonoid , Mul , One , NatCast : Type u_1

• Zero is a left absorbing element for multiplication

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

• Zero is a right absorbing element for multiplication

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

• Multiplication is associative

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

• One is a left neutral element for multiplication

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

• One is a right neutral element for multiplication

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

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

  natCast_zero : autoParam (NatCast.natCast 0 = 0) _auto✝

• The canonical map ℕ → R→ R is a homomorphism.

  natCast_succ : autoParam (∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1) _auto✝

• Raising to the power of a natural number.

  npow : ℕ → α → α

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

  npow_zero : autoParam (∀ (x : α), npow 0 x = 1) _auto✝

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

  npow_succ : autoParam (∀ (n : ℕ) (x : α), npow (n + 1) x = x * npow n x) _auto✝

• Multiplication is commutative in a commutative semigroup.

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

• No zero divisors.

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

ink

theorem mul_add_mul_le_mul_add_mul {α : Type u} [inst : StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [inst : ExistsAddOfLE α] (hab : a ≤ b) (hcd : c ≤ d) : a * d + b * c ≤ a * c + b * d

Binary rearrangement inequality.

ink

theorem mul_add_mul_le_mul_add_mul' {α : Type u} [inst : StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [inst : ExistsAddOfLE α] (hba : b ≤ a) (hdc : d ≤ c) : a • d + b • c ≤ a • c + b • d

Binary rearrangement inequality.

ink

theorem mul_add_mul_lt_mul_add_mul {α : Type u} [inst : StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [inst : ExistsAddOfLE α] (hab : a < b) (hcd : c < d) : a * d + b * c < a * c + b * d

Binary strict rearrangement inequality.

ink

theorem mul_add_mul_lt_mul_add_mul' {α : Type u} [inst : StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [inst : ExistsAddOfLE α] (hba : b < a) (hdc : d < c) : a • d + b • c < a • c + b • d

Binary rearrangement inequality.

ink

instance CanonicallyOrderedCommSemiring.toNoZeroDivisors {α : Type u} [inst : CanonicallyOrderedCommSemiring α] : NoZeroDivisors α

Equations

• @CanonicallyOrderedCommSemiring.toNoZeroDivisors = @CanonicallyOrderedCommSemiring.toNoZeroDivisors.proof_1

ink

instance CanonicallyOrderedCommSemiring.toCovariantClassMulLE {α : Type u} [inst : CanonicallyOrderedCommSemiring α] : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

Equations

• @CanonicallyOrderedCommSemiring.toCovariantClassMulLE = @CanonicallyOrderedCommSemiring.toCovariantClassMulLE.proof_1

ink

instance CanonicallyOrderedCommSemiring.toOrderedCommMonoid {α : Type u} [inst : CanonicallyOrderedCommSemiring α] : OrderedCommMonoid α

Equations

• CanonicallyOrderedCommSemiring.toOrderedCommMonoid = OrderedCommMonoid.mk (_ : ∀ (x x_1 : α), x ≤ x_1 → ∀ (a : α), a * x ≤ a * x_1)

ink

instance CanonicallyOrderedCommSemiring.toOrderedCommSemiring {α : Type u} [inst : CanonicallyOrderedCommSemiring α] : OrderedCommSemiring α

Equations

• CanonicallyOrderedCommSemiring.toOrderedCommSemiring = let src := inst; OrderedCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)

ink

@[simp]

theorem CanonicallyOrderedCommSemiring.mul_pos {α : Type u} [inst : CanonicallyOrderedCommSemiring α] {a : α} {b : α} : 0 < a * b ↔ 0 < a ∧ 0 < b

ink

theorem AddLECancellable.mul_tsub {α : Type u} [inst : CanonicallyOrderedCommSemiring α] {a : α} {b : α} {c : α} [inst : Sub α] [inst : OrderedSub α] [inst : IsTotal α fun x x_1 => x ≤ x_1] (h : AddLECancellable (a * c)) : a * (b - c) = a * b - a * c

ink

theorem AddLECancellable.tsub_mul {α : Type u} [inst : CanonicallyOrderedCommSemiring α] {a : α} {b : α} {c : α} [inst : Sub α] [inst : OrderedSub α] [inst : IsTotal α fun x x_1 => x ≤ x_1] (h : AddLECancellable (b * c)) : (a - b) * c = a * c - b * c

ink

theorem mul_tsub {α : Type u} [inst : CanonicallyOrderedCommSemiring α] [inst : Sub α] [inst : OrderedSub α] [inst : IsTotal α fun x x_1 => x ≤ x_1] [inst : 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

ink

theorem tsub_mul {α : Type u} [inst : CanonicallyOrderedCommSemiring α] [inst : Sub α] [inst : OrderedSub α] [inst : IsTotal α fun x x_1 => x ≤ x_1] [inst : 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