Mathlib.Algebra.Order.Ring.Canonical

CanonicallyOrderedCommSemiring structure

(R : Type*) extends CanonicallyOrderedAddCommMonoid R,
    CommSemiring R

Full source

/-- 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. -/
@[deprecated "Use `[OrderedCommSemiring R] [CanonicallyOrderedAdd R] [NoZeroDivisors R]` instead."
  (since := "2025-01-13")]
structure CanonicallyOrderedCommSemiring (R : Type*) extends CanonicallyOrderedAddCommMonoid R,
    CommSemiring R where
  /-- No zero divisors. -/
  protected eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : R}, a * b = 0 → a = 0 ∨ b = 0

Canonically Ordered Commutative Semiring

Informal description

A canonically ordered commutative semiring is a commutative semiring $ R $ equipped with a canonical order such that for any elements $ a, b \in R $, the inequality $ a \leq b $ holds if and only if there exists an element $ c \in R $ satisfying $ b = a + c $. This structure generalizes the natural numbers but excludes ordered groups like the integers.

CanonicallyOrderedAdd.toZeroLEOneClass instance

[AddZeroClass R] [One R] [LE R] [CanonicallyOrderedAdd R] : ZeroLEOneClass R

Full source

instance (priority := 10) CanonicallyOrderedAdd.toZeroLEOneClass
    [AddZeroClass R] [One R] [LE R] [CanonicallyOrderedAdd R] : ZeroLEOneClass R where
  zero_le_one := zero_le _

Zero is Less Than or Equal to One in Canonically Ordered Additive Structures

Informal description

For any type $R$ equipped with an addition operation, a zero element, a one element, a preorder $\leq$, and a canonically ordered additive structure, the inequality $0 \leq 1$ holds in $R$.

Odd.pos theorem

[Semiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Nontrivial R] {a : R} : Odd a → 0 < a

Full source

lemma Odd.pos [Semiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Nontrivial R] {a : R} :
    Odd a → 0 < a := by
  rintro ⟨k, rfl⟩; simp

Odd Elements are Positive in Canonically Ordered Semirings

Informal description

Let $R$ be a nontrivial semiring with a partial order and a canonically ordered additive structure. For any element $a \in R$, if $a$ is odd, then $0 < a$.

CanonicallyOrderedAdd.toMulLeftMono instance

[NonUnitalNonAssocSemiring R] [LE R] [CanonicallyOrderedAdd R] : MulLeftMono R

Full source

instance (priority := 100) toMulLeftMono [NonUnitalNonAssocSemiring R]
    [LE R] [CanonicallyOrderedAdd R] : MulLeftMono R := by
  refine ⟨fun a b c h => ?_⟩; dsimp
  rcases exists_add_of_le h with ⟨c, rfl⟩
  rw [mul_add]
  apply self_le_add_right

Monotonicity of Left Multiplication in Canonically Ordered Semirings

Informal description

For any non-unital non-associative semiring $R$ with a preorder $\leq$ that is canonically ordered as an additive monoid, left multiplication is monotone with respect to $\leq$. That is, for any $a, b_1, b_2 \in R$, if $b_1 \leq b_2$, then $a * b_1 \leq a * b_2$.

CanonicallyOrderedAdd.toIsOrderedMonoid theorem

: IsOrderedMonoid R

Full source

lemma toIsOrderedMonoid : IsOrderedMonoid R where
  mul_le_mul_left _ _ := mul_le_mul_left'

Canonically Ordered Additive Monoid is an Ordered Monoid

Informal description

For any canonically ordered additive monoid $R$, the structure $R$ forms an ordered monoid. That is, $R$ is equipped with a partial order $\leq$ such that the multiplication operation is monotone in both arguments: for any $x, y, z \in R$, if $x \leq y$, then $x \cdot z \leq y \cdot z$ and $z \cdot x \leq z \cdot y$.

CanonicallyOrderedAdd.toIsOrderedRing theorem

: IsOrderedRing R

Full source

lemma toIsOrderedRing : IsOrderedRing R where
  zero_le_one := zero_le _
  add_le_add_left _ _ := add_le_add_left
  mul_le_mul_of_nonneg_left _ _ _ h _ := mul_le_mul_left' h _
  mul_le_mul_of_nonneg_right _ _ _ h _ := mul_le_mul_right' h _

Canonically Ordered Additive Monoid Induces Ordered Semiring Structure

Informal description

Any canonically ordered additive monoid $R$ that is also a semiring with a partial order and satisfies the properties of an ordered additive monoid and the condition $0 \leq 1$ forms an ordered semiring. Specifically: 1. Addition is monotone (if $a \leq b$ then $a + c \leq b + c$ for all $c$) 2. Multiplication by nonnegative elements is monotone (if $0 \leq a$ and $b \leq c$ then $a \cdot b \leq a \cdot c$) 3. The zero element is less than or equal to the one element ($0 \leq 1$)

CanonicallyOrderedAdd.mul_pos theorem

[NoZeroDivisors R] {a b : R} : 0 < a * b ↔ 0 < a ∧ 0 < b

Full source

@[simp]
protected theorem mul_pos [NoZeroDivisors R] {a b : R} :
    0 < a * b ↔ 0 < a ∧ 0 < b := by
  simp only [pos_iff_ne_zero, ne_eq, mul_eq_zero, not_or]

Positivity of Product in Canonically Ordered Monoid Without Zero Divisors

Informal description

In a canonically ordered additive monoid $R$ with no zero divisors, the product $a \cdot b$ is positive if and only if both $a$ and $b$ are positive. That is, $0 < a \cdot b \leftrightarrow 0 < a \land 0 < b$.

CanonicallyOrderedAdd.pow_pos theorem

[NoZeroDivisors R] {a : R} (ha : 0 < a) (n : ℕ) : 0 < a ^ n

Full source

lemma pow_pos [NoZeroDivisors R] {a : R} (ha : 0 < a) (n : ℕ) : 0 < a ^ n :=
  pos_iff_ne_zero.2 <| pow_ne_zero _ ha.ne'

Positivity of Powers in Canonically Ordered Monoids Without Zero Divisors

Informal description

In a canonically ordered additive monoid $R$ with no zero divisors, if $a$ is a positive element (i.e., $0 < a$) and $n$ is a natural number, then the $n$-th power of $a$ is also positive, i.e., $0 < a^n$.

CanonicallyOrderedAdd.mul_lt_mul_of_lt_of_lt theorem

[PosMulStrictMono R] {a b c d : R} (hab : a < b) (hcd : c < d) : a * c < b * d

Full source

protected lemma mul_lt_mul_of_lt_of_lt
    [PosMulStrictMono R] {a b c d : R} (hab : a < b) (hcd : c < d) :
    a * c < b * d := by
  -- TODO: This should be an instance but it currently times out
  have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›
  obtain rfl | hc := eq_zero_or_pos c
  · rw [mul_zero]
    exact mul_pos ((zero_le _).trans_lt hab) hcd
  · exact mul_lt_mul_of_pos' hab hcd hc ((zero_le _).trans_lt hab)

Strict Inequality Preservation under Multiplication in Canonically Ordered Monoids

Informal description

Let $R$ be a canonically ordered additive monoid where left multiplication by positive elements is strictly monotone. For any elements $a, b, c, d \in R$ with $a < b$ and $c < d$, we have $a \cdot c < b \cdot d$.

AddLECancellable.mul_tsub theorem

{a b c : R} (h : AddLECancellable (a * c)) : a * (b - c) = a * b - a * c

Full source

protected theorem mul_tsub {a b c : R}
    (h : AddLECancellable (a * c)) : a * (b - c) = a * b - a * c := by
  obtain (hbc | hcb) := total_of (· ≤ ·) b c
  · rw [tsub_eq_zero_iff_le.2 hbc, mul_zero, tsub_eq_zero_iff_le.2 (mul_le_mul_left' hbc a)]
  · apply h.eq_tsub_of_add_eq
    rw [← mul_add, tsub_add_cancel_of_le hcb]

Left Multiplication Distributes Over Subtraction for Additively Cancellable Elements: $a \cdot (b - c) = a \cdot b - a \cdot c$

Informal description

Let $R$ be a canonically ordered additive monoid with subtraction, and let $a, b, c \in R$. If the element $a \cdot c$ is additively cancellable (i.e., for all $x, y \in R$, $x + a \cdot c \leq y + a \cdot c$ implies $x \leq y$), then the following equality holds: \[ a \cdot (b - c) = a \cdot b - a \cdot c. \]

AddLECancellable.tsub_mul theorem

[MulRightMono R] {a b c : R} (h : AddLECancellable (b * c)) : (a - b) * c = a * c - b * c

Full source

protected theorem tsub_mul [MulRightMono R] {a b c : R}
    (h : AddLECancellable (b * c)) : (a - b) * c = a * c - b * c := by
  obtain (hab | hba) := total_of (· ≤ ·) a b
  · rw [tsub_eq_zero_iff_le.2 hab, zero_mul, tsub_eq_zero_iff_le.2 (mul_le_mul_right' hab c)]
  · apply h.eq_tsub_of_add_eq
    rw [← add_mul, tsub_add_cancel_of_le hba]

Subtraction-Multiplication Identity in Canonically Ordered Monoids: $(a - b) \cdot c = a \cdot c - b \cdot c$ under cancellability

Informal description

Let $R$ be a canonically ordered additive monoid where right multiplication is monotone. For any elements $a, b, c \in R$ such that $b \cdot c$ is additively cancellable (i.e., $x + b \cdot c \leq y + b \cdot c$ implies $x \leq y$), we have $(a - b) \cdot c = a \cdot c - b \cdot c$.

mul_tsub theorem

(a b c : R) : a * (b - c) = a * b - a * c

Full source

theorem mul_tsub (a b c : R) : a * (b - c) = a * b - a * c :=
  Contravariant.AddLECancellable.mul_tsub

Left Multiplication Distributes Over Subtraction in Canonically Ordered Monoids: $a \cdot (b - c) = a \cdot b - a \cdot c$

Informal description

Let $R$ be a canonically ordered additive monoid with subtraction. For any elements $a, b, c \in R$, the following equality holds: \[ a \cdot (b - c) = a \cdot b - a \cdot c. \]

tsub_mul theorem

[MulRightMono R] (a b c : R) : (a - b) * c = a * c - b * c

Full source

theorem tsub_mul [MulRightMono R] (a b c : R) :
    (a - b) * c = a * c - b * c :=
  Contravariant.AddLECancellable.tsub_mul

Subtraction-Multiplication Identity in Canonically Ordered Monoids: $(a - b)c = ac - bc$

Informal description

Let $R$ be a canonically ordered additive monoid where right multiplication is monotone. For any elements $a, b, c \in R$, the following identity holds: $$(a - b) \cdot c = a \cdot c - b \cdot c.$$

mul_tsub_one theorem

[AddLeftReflectLE R] (a b : R) : a * (b - 1) = a * b - a

Full source

lemma mul_tsub_one [AddLeftReflectLE R] (a b : R) :
    a * (b - 1) = a * b - a := by rw [mul_tsub, mul_one]

Multiplication-Distributes-Over-Subtraction-by-One Identity: $a \cdot (b - 1) = a \cdot b - a$

Informal description

Let $R$ be a canonically ordered additive monoid where addition reflects the order from the left. For any elements $a, b \in R$, the following equality holds: \[ a \cdot (b - 1) = a \cdot b - a. \]

tsub_one_mul theorem

[MulRightMono R] [AddLeftReflectLE R] (a b : R) : (a - 1) * b = a * b - b

Full source

lemma tsub_one_mul [MulRightMono R] [AddLeftReflectLE R] (a b : R) :
    (a - 1) * b = a * b - b := by rw [tsub_mul, one_mul]

Subtraction-Identity Multiplication Identity: $(a - 1)b = ab - b$

Informal description

Let $R$ be a canonically ordered additive monoid where right multiplication is monotone and addition reflects the order from the left. For any elements $a, b \in R$, the following identity holds: $$(a - 1) \cdot b = a \cdot b - b.$$

mul_self_tsub_mul_self theorem

(a b : R) : a * a - b * b = (a + b) * (a - b)

Full source

/-- The `tsub` version of `mul_self_sub_mul_self`. Notably, this holds for `Nat` and `NNReal`. -/
theorem mul_self_tsub_mul_self (a b : R) :
    a * a - b * b = (a + b) * (a - b) := by
  rw [mul_tsub, add_mul, add_mul, tsub_add_eq_tsub_tsub, mul_comm b a, add_tsub_cancel_right]

Difference of Squares Identity: $a^2 - b^2 = (a + b)(a - b)$

Informal description

For any elements $a$ and $b$ in a canonically ordered additive monoid $R$ with subtraction, the difference of squares identity holds: \[ a^2 - b^2 = (a + b)(a - b). \]

sq_tsub_sq theorem

(a b : R) : a ^ 2 - b ^ 2 = (a + b) * (a - b)

Full source

/-- The `tsub` version of `sq_sub_sq`. Notably, this holds for `Nat` and `NNReal`. -/
theorem sq_tsub_sq (a b : R) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := by
  rw [sq, sq, mul_self_tsub_mul_self]

Difference of Squares Identity: $a^2 - b^2 = (a + b)(a - b)$

Informal description

For any elements $a$ and $b$ in a canonically ordered additive monoid $R$ with subtraction, the difference of squares identity holds: \[ a^2 - b^2 = (a + b)(a - b). \]

mul_self_tsub_one theorem

(a : R) : a * a - 1 = (a + 1) * (a - 1)

Full source

theorem mul_self_tsub_one (a : R) : a * a - 1 = (a + 1) * (a - 1) := by
  rw [← mul_self_tsub_mul_self, mul_one]

Difference of Squares Identity: $a^2 - 1 = (a + 1)(a - 1)$

Informal description

For any element $a$ in a canonically ordered additive monoid $R$ with subtraction, the following identity holds: \[ a^2 - 1 = (a + 1)(a - 1). \]