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_1) extends CanonicallyOrderedAddCommMonoid , CommSemiring , OrderedAddCommMonoid , OrderBot , Semiring , CommMonoid , NonUnitalSemiring , NonAssocSemiring , MonoidWithZero , NonUnitalNonAssocSemiring , Monoid , MulZeroOneClass , SemigroupWithZero , AddCommMonoidWithOne , CommSemigroup , MulOneClass , AddMonoidWithOne , AddCommMonoid , PartialOrder , Distrib , Semigroup , MulZeroClass , NatCast , AddMonoid , One , AddCommSemigroup , AddSemigroup , AddZeroClass , CommMagma , Mul , Zero , AddCommMagma , Add , Preorder , LE , LT , Bot : Type u_1

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.

theorem CanonicallyOrderedCommSemiring.eq_zero_or_eq_zero_of_mul_eq_zero {α : Type u_1} [self : CanonicallyOrderedCommSemiring α] {a : α} {b : α} : a * b = 0 → a = 0 ∨ b = 0

No zero divisors.

theorem Odd.pos {α : Type u} [CanonicallyOrderedCommSemiring α] {a : α} [Nontrivial α] : Odd a → 0 < a

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

instance CanonicallyOrderedCommSemiring.toMulLeftMono {α : Type u} [CanonicallyOrderedCommSemiring α] : MulLeftMono α

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• CanonicallyOrderedCommSemiring.toOrderedCommMonoid = OrderedCommMonoid.mk ⋯

@[instance 100]

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

Equations

• CanonicallyOrderedCommSemiring.toOrderedCommSemiring = OrderedCommSemiring.mk ⋯

@[simp]

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

theorem CanonicallyOrderedCommSemiring.pow_pos {α : Type u} [CanonicallyOrderedCommSemiring α] {a : α} (ha : 0 < a) (n : ℕ) : 0 < a ^ n

theorem CanonicallyOrderedCommSemiring.mul_lt_mul_of_lt_of_lt {α : Type u} [CanonicallyOrderedCommSemiring α] {a : α} {b : α} {c : α} {d : α} [PosMulStrictMono α] (hab : a < b) (hcd : c < d) : a * c < b * d

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

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

theorem mul_tsub {α : Type u} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [AddLeftReflectLE α] (a : α) (b : α) (c : α) : a * (b - c) = a * b - a * c

theorem tsub_mul {α : Type u} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [AddLeftReflectLE α] (a : α) (b : α) (c : α) : (a - b) * c = a * c - b * c

theorem mul_tsub_one {α : Type u} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [AddLeftReflectLE α] (a : α) (b : α) : a * (b - 1) = a * b - a

theorem tsub_one_mul {α : Type u} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [AddLeftReflectLE α] (a : α) (b : α) : (a - 1) * b = a * b - b

theorem mul_self_tsub_mul_self {α : Type u} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [AddLeftReflectLE α] (a : α) (b : α) : a * a - b * b = (a + b) * (a - b)

The tsub version of mul_self_sub_mul_self. Notably, this holds for Nat and NNReal.

theorem sq_tsub_sq {α : Type u} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [AddLeftReflectLE α] (a : α) (b : α) : a ^ 2 - b ^ 2 = (a + b) * (a - b)

The tsub version of sq_sub_sq. Notably, this holds for Nat and NNReal.

theorem mul_self_tsub_one {α : Type u} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [AddLeftReflectLE α] (a : α) : a * a - 1 = (a + 1) * (a - 1)