Canonically ordered rings and semirings.

@[deprecated "Use `[OrderedCommSemiring α] [CanonicallyOrderedAdd α] [NoZeroDivisors α]` instead." (since := "2025-01-13")]

structure CanonicallyOrderedCommSemiring (α : Type u_1) extends CanonicallyOrderedAddCommMonoid α, CommSemiring α : 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.

• 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 : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• 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 (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
• 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
• natCast : ℕ → α
• natCast_zero : NatCast.natCast 0 = 0
• natCast_succ (n : ℕ) : NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : self.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : self.npow (n + 1) x = self.npow n x * x
• 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

  No zero divisors.

@[instance 10]

instance CanonicallyOrderedAdd.toZeroLEOneClass {α : Type u} [AddZeroClass α] [One α] [LE α] [CanonicallyOrderedAdd α] : ZeroLEOneClass α

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

@[instance 100]

instance CanonicallyOrderedAdd.toMulLeftMono {α : Type u} [NonUnitalNonAssocSemiring α] [LE α] [CanonicallyOrderedAdd α] : MulLeftMono α

@[reducible, inline]

abbrev CanonicallyOrderedAdd.toOrderedCommMonoid {α : Type u} [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] : OrderedCommMonoid α

Construct an OrderedCommMonoid from a canonically ordered CommSemiring.

Equations

• CanonicallyOrderedAdd.toOrderedCommMonoid = OrderedCommMonoid.mk ⋯

@[reducible, inline]

abbrev CanonicallyOrderedAdd.toOrderedCommSemiring {α : Type u} [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] : OrderedCommSemiring α

Construct an OrderedCommSemiring from a canonically ordered CommSemiring.

Equations

• CanonicallyOrderedAdd.toOrderedCommSemiring = OrderedCommSemiring.mk ⋯

@[simp]

theorem CanonicallyOrderedAdd.mul_pos {α : Type u} [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] {a b : α} : 0 < a * b ↔ 0 < a ∧ 0 < b

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

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

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

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

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

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

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

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

theorem mul_self_tsub_mul_self {α : Type u} [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [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} [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [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} [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [AddLeftReflectLE α] (a : α) : a * a - 1 = (a + 1) * (a - 1)