# Basic facts for ordered rings and semirings #

This file develops the basics of ordered (semi)rings in an unbundled fashion for later use with the bundled classes from `Mathlib/Algebra/Order/Ring/Defs.lean`.

The set of typeclass variables here comprises

- an algebraic class (`Semiring`, `CommSemiring`, `Ring`, `CommRing`)
- an order class (`PartialOrder`, `LinearOrder`)
- assumptions on how both interact ((strict) monotonicity, canonicity)

For short,

- "`+` respects `≤`" means "monotonicity of addition"
- "`+` respects `<`" means "strict monotonicity of addition"
- "`*` respects `≤`" means "monotonicity of multiplication by a nonnegative number".
- "`*` respects `<`" means "strict monotonicity of multiplication by a positive number".

## Typeclasses found in `Algebra.Order.Ring.Defs` #

- `OrderedSemiring`: Semiring with a partial order such that `+` and `*` respect `≤`.
- `StrictOrderedSemiring`: Nontrivial semiring with a partial order such that `+` and `*` respects `<`.
- `OrderedCommSemiring`: Commutative semiring with a partial order such that `+` and `*` respect `≤`.
- `StrictOrderedCommSemiring`: Nontrivial commutative semiring with a partial order such that `+` and `*` respect `<`.
- `OrderedRing`: Ring with a partial order such that `+` respects `≤` and `*` respects `<`.
- `OrderedCommRing`: Commutative ring with a partial order such that `+` respects `≤` and `*` respects `<`.
- `LinearOrderedSemiring`: Nontrivial semiring with a linear order such that `+` respects `≤` and `*` respects `<`.
- `LinearOrderedCommSemiring`: Nontrivial commutative semiring with a linear order such that `+` respects `≤` and `*` respects `<`.
- `LinearOrderedRing`: Nontrivial ring with a linear order such that `+` respects `≤` and `*` respects `<`.
- `LinearOrderedCommRing`: Nontrivial commutative ring with a linear order such that `+` respects `≤` and `*` respects `<`.
- `CanonicallyOrderedCommSemiring`: Commutative semiring with a partial order such that `+` respects `≤`, `*` respects `<`, and `a ≤ b ↔ ∃ c, b = a + c`.

## Hierarchy #

The hardest part of proving order lemmas might be to figure out the correct generality and its corresponding typeclass. Here's an attempt at demystifying it. For each typeclass, we list its immediate predecessors and what conditions are added to each of them.

- `OrderedSemiring`
  - `OrderedAddCommMonoid` & multiplication & `*` respects `≤`
  - `Semiring` & partial order structure & `+` respects `≤` & `*` respects `≤`
- `StrictOrderedSemiring`
  - `OrderedCancelAddCommMonoid` & multiplication & `*` respects `<` & nontriviality
  - `OrderedSemiring` & `+` respects `<` & `*` respects `<` & nontriviality
- `OrderedCommSemiring`
  - `OrderedSemiring` & commutativity of multiplication
  - `CommSemiring` & partial order structure & `+` respects `≤` & `*` respects `<`
- `StrictOrderedCommSemiring`
  - `StrictOrderedSemiring` & commutativity of multiplication
  - `OrderedCommSemiring` & `+` respects `<` & `*` respects `<` & nontriviality
- `OrderedRing`
  - `OrderedSemiring` & additive inverses
  - `OrderedAddCommGroup` & multiplication & `*` respects `<`
  - `Ring` & partial order structure & `+` respects `≤` & `*` respects `<`
- `StrictOrderedRing`
  - `StrictOrderedSemiring` & additive inverses
  - `OrderedSemiring` & `+` respects `<` & `*` respects `<` & nontriviality
- `OrderedCommRing`
  - `OrderedRing` & commutativity of multiplication
  - `OrderedCommSemiring` & additive inverses
  - `CommRing` & partial order structure & `+` respects `≤` & `*` respects `<`
- `StrictOrderedCommRing`
  - `StrictOrderedCommSemiring` & additive inverses
  - `StrictOrderedRing` & commutativity of multiplication
  - `OrderedCommRing` & `+` respects `<` & `*` respects `<` & nontriviality
- `LinearOrderedSemiring`
  - `StrictOrderedSemiring` & totality of the order
  - `LinearOrderedAddCommMonoid` & multiplication & nontriviality & `*` respects `<`
- `LinearOrderedCommSemiring`
  - `StrictOrderedCommSemiring` & totality of the order
  - `LinearOrderedSemiring` & commutativity of multiplication
- `LinearOrderedRing`
  - `StrictOrderedRing` & totality of the order
  - `LinearOrderedSemiring` & additive inverses
  - `LinearOrderedAddCommGroup` & multiplication & `*` respects `<`
  - `Ring` & `IsDomain` & linear order structure
- `LinearOrderedCommRing`
  - `StrictOrderedCommRing` & totality of the order
  - `LinearOrderedRing` & commutativity of multiplication
  - `LinearOrderedCommSemiring` & additive inverses
  - `CommRing` & `IsDomain` & linear order structure

## Generality #

Each section is labelled with a corresponding bundled ordered ring typeclass in mind. Mixins for relating the order structures and ring structures are added as needed.

TODO: the mixin assumptions can be relaxed in most cases

Note that `OrderDual` does not satisfy any of the ordered ring typeclasses due to the `zero_le_one` field.

source
theorem add_one_le_two_mul {R : Type u} [LE R] [NonAssocSemiring R] [AddLeftMono R] {a : R} (a1 : 1 ≤ a) :
a + 1 ≤ 2 * a
source
theorem add_le_mul_two_add {R : Type u} [Semiring R] [Preorder R] {a b : R} [ZeroLEOneClass R] [MulPosMono R] [AddLeftMono R] (a2 : 2 ≤ a) (b0 : 0 ≤ b) :
a + (2 + b) ≤ a * (2 + b)
source
theorem mul_le_mul_of_nonpos_left {R : Type u} [Semiring R] [Preorder R] {a b c : R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (h : b ≤ a) (hc : c ≤ 0) :
c * a ≤ c * b
source
theorem mul_le_mul_of_nonpos_right {R : Type u} [Semiring R] [Preorder R] {a b c : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (h : b ≤ a) (hc : c ≤ 0) :
a * c ≤ b * c
source
theorem mul_nonneg_of_nonpos_of_nonpos {R : Type u} [Semiring R] [Preorder R] {a b : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (ha : a ≤ 0) (hb : b ≤ 0) :
0 ≤ a * b
source
theorem mul_le_mul_of_nonneg_of_nonpos {R : Type u} [Semiring R] [Preorder R] {a b c d : R} [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hca : c ≤ a) (hbd : b ≤ d) (hc : 0 ≤ c) (hb : b ≤ 0) :
a * b ≤ c * d
source
theorem mul_le_mul_of_nonneg_of_nonpos' {R : Type u} [Semiring R] [Preorder R] {a b c d : R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hca : c ≤ a) (hbd : b ≤ d) (ha : 0 ≤ a) (hd : d ≤ 0) :
a * b ≤ c * d
source
theorem mul_le_mul_of_nonpos_of_nonneg {R : Type u} [Semiring R] [Preorder R] {a b c d : R} [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hac : a ≤ c) (hdb : d ≤ b) (hc : c ≤ 0) (hb : 0 ≤ b) :
a * b ≤ c * d
source
theorem mul_le_mul_of_nonpos_of_nonneg' {R : Type u} [Semiring R] [Preorder R] {a b c d : R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hca : c ≤ a) (hbd : b ≤ d) (ha : 0 ≤ a) (hd : d ≤ 0) :
a * b ≤ c * d
source
theorem mul_le_mul_of_nonpos_of_nonpos {R : Type u} [Semiring R] [Preorder R] {a b c d : R} [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hca : c ≤ a) (hdb : d ≤ b) (hc : c ≤ 0) (hb : b ≤ 0) :
a * b ≤ c * d
source
theorem mul_le_mul_of_nonpos_of_nonpos' {R : Type u} [Semiring R] [Preorder R] {a b c d : R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hca : c ≤ a) (hdb : d ≤ b) (ha : a ≤ 0) (hd : d ≤ 0) :
a * b ≤ c * d
source
theorem le_mul_of_le_one_left {R : Type u} [Semiring R] [Preorder R] {a b : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hb : b ≤ 0) (h : a ≤ 1) :
b ≤ a * b

Variant of `mul_le_of_le_one_left` for `b` non-positive instead of non-negative.

source
theorem mul_le_of_one_le_left {R : Type u} [Semiring R] [Preorder R] {a b : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hb : b ≤ 0) (h : 1 ≤ a) :
a * b ≤ b

Variant of `le_mul_of_one_le_left` for `b` non-positive instead of non-negative.

source
theorem le_mul_of_le_one_right {R : Type u} [Semiring R] [Preorder R] {a b : R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (ha : a ≤ 0) (h : b ≤ 1) :
a ≤ a * b

Variant of `mul_le_of_le_one_right` for `a` non-positive instead of non-negative.

source
theorem mul_le_of_one_le_right {R : Type u} [Semiring R] [Preorder R] {a b : R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (ha : a ≤ 0) (h : 1 ≤ b) :
a * b ≤ a

Variant of `le_mul_of_one_le_right` for `a` non-positive instead of non-negative.

source
theorem antitone_mul_left {R : Type u} [Semiring R] [Preorder R] [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] {a : R} (ha : a ≤ 0) :
Antitone fun (x : R) => a * x
source
theorem antitone_mul_right {R : Type u} [Semiring R] [Preorder R] [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] {a : R} (ha : a ≤ 0) :
Antitone fun (x : R) => x * a
source
theorem Monotone.const_mul_of_nonpos {R : Type u} {α : Type u_1} [Semiring R] [Preorder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Monotone f) (ha : a ≤ 0) :
Antitone fun (x : α) => a * f x
source
theorem Monotone.mul_const_of_nonpos {R : Type u} {α : Type u_1} [Semiring R] [Preorder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Monotone f) (ha : a ≤ 0) :
Antitone fun (x : α) => f x * a
source
theorem Antitone.const_mul_of_nonpos {R : Type u} {α : Type u_1} [Semiring R] [Preorder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Antitone f) (ha : a ≤ 0) :
Monotone fun (x : α) => a * f x
source
theorem Antitone.mul_const_of_nonpos {R : Type u} {α : Type u_1} [Semiring R] [Preorder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Antitone f) (ha : a ≤ 0) :
Monotone fun (x : α) => f x * a
source
theorem Antitone.mul_monotone {R : Type u} {α : Type u_1} [Semiring R] [Preorder R] [Preorder α] {f g : α → R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Antitone f) (hg : Monotone g) (hf₀ : ∀ (x : α), f x ≤ 0) (hg₀ : ∀ (x : α), 0 ≤ g x) :
Antitone (f * g)
source
theorem Monotone.mul_antitone {R : Type u} {α : Type u_1} [Semiring R] [Preorder R] [Preorder α] {f g : α → R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Monotone f) (hg : Antitone g) (hf₀ : ∀ (x : α), 0 ≤ f x) (hg₀ : ∀ (x : α), g x ≤ 0) :
Antitone (f * g)
source
theorem Antitone.mul {R : Type u} {α : Type u_1} [Semiring R] [Preorder R] [Preorder α] {f g : α → R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Antitone f) (hg : Antitone g) (hf₀ : ∀ (x : α), f x ≤ 0) (hg₀ : ∀ (x : α), g x ≤ 0) :
Monotone (f * g)
source
theorem lt_two_mul_self {R : Type u} [Semiring R] [PartialOrder R] {a : R} [ZeroLEOneClass R] [MulPosStrictMono R] [NeZero 1] [AddLeftStrictMono R] (ha : 0 < a) :
a < 2 * a
source
theorem mul_lt_mul_of_neg_left {R : Type u} [Semiring R] [PartialOrder R] {a b c : R} [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (h : b < a) (hc : c < 0) :
c * a < c * b
source
theorem mul_lt_mul_of_neg_right {R : Type u} [Semiring R] [PartialOrder R] {a b c : R} [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (h : b < a) (hc : c < 0) :
a * c < b * c
source
theorem mul_pos_of_neg_of_neg {R : Type u} [Semiring R] [PartialOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] {a b : R} (ha : a < 0) (hb : b < 0) :
0 < a * b
source
theorem lt_mul_of_lt_one_left {R : Type u} [Semiring R] [PartialOrder R] {a b : R} [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hb : b < 0) (h : a < 1) :
b < a * b

Variant of `mul_lt_of_lt_one_left` for `b` negative instead of positive.

source
theorem mul_lt_of_one_lt_left {R : Type u} [Semiring R] [PartialOrder R] {a b : R} [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hb : b < 0) (h : 1 < a) :
a * b < b

Variant of `lt_mul_of_one_lt_left` for `b` negative instead of positive.

source
theorem lt_mul_of_lt_one_right {R : Type u} [Semiring R] [PartialOrder R] {a b : R} [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (ha : a < 0) (h : b < 1) :
a < a * b

Variant of `mul_lt_of_lt_one_right` for `a` negative instead of positive.

source
theorem mul_lt_of_one_lt_right {R : Type u} [Semiring R] [PartialOrder R] {a b : R} [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (ha : a < 0) (h : 1 < b) :
a * b < a

Variant of `lt_mul_of_lt_one_right` for `a` negative instead of positive.

source
theorem strictAnti_mul_left {R : Type u} [Semiring R] [PartialOrder R] [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] {a : R} (ha : a < 0) :
StrictAnti fun (x : R) => a * x
source
theorem strictAnti_mul_right {R : Type u} [Semiring R] [PartialOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] {a : R} (ha : a < 0) :
StrictAnti fun (x : R) => x * a
source
theorem StrictMono.const_mul_of_neg {R : Type u} {α : Type u_1} [Semiring R] [PartialOrder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hf : StrictMono f) (ha : a < 0) :
StrictAnti fun (x : α) => a * f x
source
theorem StrictMono.mul_const_of_neg {R : Type u} {α : Type u_1} [Semiring R] [PartialOrder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hf : StrictMono f) (ha : a < 0) :
StrictAnti fun (x : α) => f x * a
source
theorem StrictAnti.const_mul_of_neg {R : Type u} {α : Type u_1} [Semiring R] [PartialOrder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hf : StrictAnti f) (ha : a < 0) :
StrictMono fun (x : α) => a * f x
source
theorem StrictAnti.mul_const_of_neg {R : Type u} {α : Type u_1} [Semiring R] [PartialOrder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hf : StrictAnti f) (ha : a < 0) :
StrictMono fun (x : α) => f x * a
source
theorem mul_add_mul_le_mul_add_mul {R : Type u} [Semiring R] [PartialOrder R] {a b c d : R} [ExistsAddOfLE R] [MulPosMono R] [AddLeftMono R] [AddLeftReflectLE R] (hab : a ≤ b) (hcd : c ≤ d) :
a * d + b * c ≤ a * c + b * d

Binary rearrangement inequality.

source
theorem mul_add_mul_le_mul_add_mul' {R : Type u} [Semiring R] [PartialOrder R] {a b c d : R} [ExistsAddOfLE R] [MulPosMono R] [AddLeftMono R] [AddLeftReflectLE R] (hba : b ≤ a) (hdc : d ≤ c) :
a * d + b * c ≤ a * c + b * d

Binary rearrangement inequality.

source
theorem mul_add_mul_lt_mul_add_mul {R : Type u} [Semiring R] [PartialOrder R] {a b c d : R} [AddLeftReflectLT R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftStrictMono R] (hab : a < b) (hcd : c < d) :
a * d + b * c < a * c + b * d

Binary strict rearrangement inequality.

source
theorem mul_add_mul_lt_mul_add_mul' {R : Type u} [Semiring R] [PartialOrder R] {a b c d : R} [AddLeftReflectLT R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftStrictMono R] (hba : b < a) (hdc : d < c) :
a * d + b * c < a * c + b * d

Binary rearrangement inequality.

source
theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [MulPosStrictMono R] [PosMulStrictMono R] (hab : 0 ≤ a * b) :
0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
source
theorem nonneg_of_mul_nonneg_left {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [MulPosStrictMono R] (h : 0 ≤ a * b) (hb : 0 < b) :
0 ≤ a
source
theorem nonneg_of_mul_nonneg_right {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [PosMulStrictMono R] (h : 0 ≤ a * b) (ha : 0 < a) :
0 ≤ b
source
theorem nonpos_of_mul_nonpos_left {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [PosMulStrictMono R] (h : a * b ≤ 0) (hb : 0 < b) :
a ≤ 0
source
theorem nonpos_of_mul_nonpos_right {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [PosMulStrictMono R] (h : a * b ≤ 0) (ha : 0 < a) :
b ≤ 0
source
@[simp]
theorem mul_nonneg_iff_of_pos_left {R : Type u} [Semiring R] [LinearOrder R] {b c : R} [PosMulStrictMono R] (h : 0 < c) :
0 ≤ c * b ↔ 0 ≤ b
source
@[simp]
theorem mul_nonneg_iff_of_pos_right {R : Type u} [Semiring R] [LinearOrder R] {b c : R} [MulPosStrictMono R] (h : 0 < c) :
0 ≤ b * c ↔ 0 ≤ b
source
theorem add_le_mul_of_left_le_right {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [ZeroLEOneClass R] [NeZero 1] [MulPosStrictMono R] [AddLeftMono R] (a2 : 2 ≤ a) (ab : a ≤ b) :
a + b ≤ a * b
source
theorem add_le_mul_of_right_le_left {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [ZeroLEOneClass R] [NeZero 1] [AddLeftMono R] [PosMulStrictMono R] (b2 : 2 ≤ b) (ba : b ≤ a) :
a + b ≤ a * b
source
theorem add_le_mul {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [ZeroLEOneClass R] [NeZero 1] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R] (a2 : 2 ≤ a) (b2 : 2 ≤ b) :
a + b ≤ a * b
source
theorem add_le_mul' {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [ZeroLEOneClass R] [NeZero 1] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R] (a2 : 2 ≤ a) (b2 : 2 ≤ b) :
a + b ≤ b * a
source
theorem mul_nonneg_iff_right_nonneg_of_pos {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [PosMulStrictMono R] (ha : 0 < a) :
0 ≤ a * b ↔ 0 ≤ b
source
theorem mul_nonneg_iff_left_nonneg_of_pos {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [PosMulStrictMono R] [MulPosStrictMono R] (hb : 0 < b) :
0 ≤ a * b ↔ 0 ≤ a
source
theorem nonpos_of_mul_nonneg_left {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [PosMulStrictMono R] (h : 0 ≤ a * b) (hb : b < 0) :
a ≤ 0
source
theorem nonpos_of_mul_nonneg_right {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [MulPosStrictMono R] (h : 0 ≤ a * b) (ha : a < 0) :
b ≤ 0
source
@[simp]
theorem Units.inv_pos {R : Type u} [Semiring R] [LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [PosMulStrictMono R] {u : R ˣ} :
0 < ↑u⁻¹ ↔ 0 < ↑u
source
@[simp]
theorem Units.inv_neg {R : Type u} [Semiring R] [LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [MulPosMono R] [PosMulMono R] {u : R ˣ} :
↑u⁻¹ < 0 ↔ ↑u < 0
source
theorem cmp_mul_pos_left {R : Type u} [Semiring R] [LinearOrder R] {a : R} [PosMulStrictMono R] (ha : 0 < a) (b c : R) :
cmp (a * b) (a * c) = cmp b c
source
theorem cmp_mul_pos_right {R : Type u} [Semiring R] [LinearOrder R] {a : R} [MulPosStrictMono R] (ha : 0 < a) (b c : R) :
cmp (b * a) (c * a) = cmp b c
source
theorem mul_max_of_nonneg {R : Type u} [Semiring R] [LinearOrder R] {a : R} [PosMulMono R] (b c : R) (ha : 0 ≤ a) :
a * max b c = max (a * b) (a * c)
source
theorem mul_min_of_nonneg {R : Type u} [Semiring R] [LinearOrder R] {a : R} [PosMulMono R] (b c : R) (ha : 0 ≤ a) :
a * min b c = min (a * b) (a * c)
source
theorem max_mul_of_nonneg {R : Type u} [Semiring R] [LinearOrder R] {c : R} [MulPosMono R] (a b : R) (hc : 0 ≤ c) :
max a b * c = max (a * c) (b * c)
source
theorem min_mul_of_nonneg {R : Type u} [Semiring R] [LinearOrder R] {c : R} [MulPosMono R] (a b : R) (hc : 0 ≤ c) :
min a b * c = min (a * c) (b * c)
source
theorem le_of_mul_le_of_one_le {R : Type u} [Semiring R] [LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [MulPosStrictMono R] [PosMulMono R] {a b c : R} (h : a * c ≤ b) (hb : 0 ≤ b) (hc : 1 ≤ c) :
a ≤ b
source
theorem nonneg_le_nonneg_of_sq_le_sq {R : Type u} [Semiring R] [LinearOrder R] [PosMulStrictMono R] [MulPosMono R] {a b : R} (hb : 0 ≤ b) (h : a * a ≤ b * b) :
a ≤ b
source
theorem mul_self_le_mul_self_iff {R : Type u} [Semiring R] [LinearOrder R] [PosMulStrictMono R] [MulPosMono R] {a b : R} (h1 : 0 ≤ a) (h2 : 0 ≤ b) :
a ≤ b ↔ a * a ≤ b * b
source
theorem mul_self_lt_mul_self_iff {R : Type u} [Semiring R] [LinearOrder R] [PosMulStrictMono R] [MulPosMono R] {a b : R} (h1 : 0 ≤ a) (h2 : 0 ≤ b) :
a < b ↔ a * a < b * b
source
theorem mul_self_inj {R : Type u} [Semiring R] [LinearOrder R] [PosMulStrictMono R] [MulPosMono R] {a b : R} (h1 : 0 ≤ a) (h2 : 0 ≤ b) :
a * a = b * b ↔ a = b
source
theorem sign_cases_of_C_mul_pow_nonneg {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [PosMulStrictMono R] (h : ∀ (n : ℕ), 0 ≤ a * b ^ n) :
a = 0 ∨ 0 < a ∧ 0 ≤ b
source
theorem mul_pos_iff {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftStrictMono R] [AddLeftReflectLT R] :
0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
source
theorem mul_nonneg_iff {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] :
0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
source
theorem mul_nonneg_of_three {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] (a b c : R) :
0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Out of three elements of a `LinearOrderedRing`, two must have the same sign.

source
theorem mul_nonneg_iff_pos_imp_nonneg {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] :
0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)
source
@[simp]
theorem mul_le_mul_left_of_neg {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightMono R] [AddRightReflectLE R] {a b c : R} (h : c < 0) :
c * a ≤ c * b ↔ b ≤ a
source
@[simp]
theorem mul_le_mul_right_of_neg {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightMono R] [AddRightReflectLE R] {a b c : R} (h : c < 0) :
a * c ≤ b * c ↔ b ≤ a
source
@[simp]
theorem mul_lt_mul_left_of_neg {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] {a b c : R} (h : c < 0) :
c * a < c * b ↔ b < a
source
@[simp]
theorem mul_lt_mul_right_of_neg {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] {a b c : R} (h : c < 0) :
a * c < b * c ↔ b < a
source
theorem lt_of_mul_lt_mul_of_nonpos_left {R : Type u} [Semiring R] [LinearOrder R] {a b c : R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (h : c * a < c * b) (hc : c ≤ 0) :
b < a
source
theorem lt_of_mul_lt_mul_of_nonpos_right {R : Type u} [Semiring R] [LinearOrder R] {a b c : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (h : a * c < b * c) (hc : c ≤ 0) :
b < a
source
theorem cmp_mul_neg_left {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightReflectLT R] [AddRightStrictMono R] {a : R} (ha : a < 0) (b c : R) :
cmp (a * b) (a * c) = cmp c b
source
theorem cmp_mul_neg_right {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightReflectLT R] [AddRightStrictMono R] {a : R} (ha : a < 0) (b c : R) :
cmp (b * a) (c * a) = cmp c b
source
@[simp]
theorem mul_self_pos {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftStrictMono R] [AddLeftReflectLT R] {a : R} :
0 < a * a ↔ a ≠ 0
source
theorem nonneg_of_mul_nonpos_left {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightMono R] [AddRightReflectLE R] {a b : R} (h : a * b ≤ 0) (hb : b < 0) :
0 ≤ a
source
theorem nonneg_of_mul_nonpos_right {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightMono R] [AddRightReflectLE R] {a b : R} (h : a * b ≤ 0) (ha : a < 0) :
0 ≤ b
source
theorem pos_of_mul_neg_left {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] {a b : R} (h : a * b < 0) (hb : b ≤ 0) :
0 < a
source
theorem pos_of_mul_neg_right {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] {a b : R} (h : a * b < 0) (ha : a ≤ 0) :
0 < b
source
theorem neg_iff_pos_of_mul_neg {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hab : a * b < 0) :
a < 0 ↔ 0 < b
source
theorem pos_iff_neg_of_mul_neg {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hab : a * b < 0) :
0 < a ↔ b < 0
source
theorem sq_nonneg {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] (a : R) :
0 ≤ a ^ 2
source
@[simp]
theorem sq_nonpos_iff {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] [NoZeroDivisors R] (r : R) :
r ^ 2 ≤ 0 ↔ r = 0
source
theorem pow_two_nonneg {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] (a : R) :
0 ≤ a ^ 2

Alias of `sq_nonneg`.

source
theorem mul_self_nonneg {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] (a : R) :
0 ≤ a * a
source
theorem mul_self_add_mul_self_eq_zero {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [NoZeroDivisors R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] :
a * a + b * b = 0 ↔ a = 0 ∧ b = 0

The sum of two squares is zero iff both elements are zero.

source
theorem eq_zero_of_mul_self_add_mul_self_eq_zero {R : Type u} [Semiring R] [LinearOrder R] {a b : R} [NoZeroDivisors R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] (h : a * a + b * b = 0) :
a = 0
source
theorem max_mul_mul_le_max_mul_max {R : Type u} [CommSemiring R] [LinearOrder R] {a d : R} [PosMulMono R] [MulPosMono R] (b c : R) (ha : 0 ≤ a) (hd : 0 ≤ d) :
max (a * b) (d * c) ≤ max a c * max d b
source
theorem two_mul_le_add_sq {R : Type u} [CommSemiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] (a b : R) :
2 * a * b ≤ a ^ 2 + b ^ 2

Binary, squared, and division-free arithmetic mean-geometric mean inequality (aka AM-GM inequality) for linearly ordered commutative semirings.

source
theorem two_mul_le_add_pow_two {R : Type u} [CommSemiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] (a b : R) :
2 * a * b ≤ a ^ 2 + b ^ 2

Alias of `two_mul_le_add_sq`.

Binary, squared, and division-free arithmetic mean-geometric mean inequality (aka AM-GM inequality) for linearly ordered commutative semirings.

source
theorem four_mul_le_sq_add {R : Type u} [CommSemiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] (a b : R) :
4 * a * b ≤ (a + b) ^ 2

Binary, squared, and division-free arithmetic mean-geometric mean inequality (aka AM-GM inequality) for linearly ordered commutative semirings.

source
theorem four_mul_le_pow_two_add {R : Type u} [CommSemiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] (a b : R) :
4 * a * b ≤ (a + b) ^ 2

Alias of `four_mul_le_sq_add`.

Binary, squared, and division-free arithmetic mean-geometric mean inequality (aka AM-GM inequality) for linearly ordered commutative semirings.

source
theorem two_mul_le_add_of_sq_eq_mul {R : Type u} [CommSemiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] {a b r : R} (ha : 0 ≤ a) (hb : 0 ≤ b) (ht : r ^ 2 = a * b) :
2 * r ≤ a + b

Binary and division-free arithmetic mean-geometric mean inequality (aka AM-GM inequality) for linearly ordered commutative semirings.

source
theorem mul_neg_iff {R : Type u} [Ring R] [LinearOrder R] {a b : R} [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftReflectLT R] [AddLeftStrictMono R] :
a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
source
theorem mul_nonpos_iff {R : Type u} [Ring R] [LinearOrder R] {a b : R} [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] :
a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
source
theorem mul_nonneg_iff_neg_imp_nonpos {R : Type u} [Ring R] [LinearOrder R] {a b : R} [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] :
0 ≤ a * b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
source
theorem mul_nonpos_iff_pos_imp_nonpos {R : Type u} [Ring R] [LinearOrder R] {a b : R} [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] :
a * b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
source
theorem mul_nonpos_iff_neg_imp_nonneg {R : Type u} [Ring R] [LinearOrder R] {a b : R} [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] :
a * b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
source
theorem neg_one_lt_zero {R : Type u} [Ring R] [LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [AddLeftStrictMono R] :
-1 < 0
source
theorem sub_one_lt {R : Type u} [Ring R] [LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [AddLeftStrictMono R] (a : R) :
a - 1 < a
source
theorem mul_self_le_mul_self_of_le_of_neg_le {R : Type u} [Ring R] [LinearOrder R] {a b : R} [MulPosMono R] [PosMulMono R] [AddLeftMono R] (h₁ : a ≤ b) (h₂ : -a ≤ b) :
a * a ≤ b * b
source
theorem sub_mul_sub_nonneg_iff {R : Type u} [Ring R] [LinearOrder R] {a b : R} [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R] (x : R) (h : a ≤ b) :
0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x
source
theorem sub_mul_sub_nonpos_iff {R : Type u} [Ring R] [LinearOrder R] {a b : R} [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R] (x : R) (h : a ≤ b) :
(x - a) * (x - b) ≤ 0 ↔ a ≤ x ∧ x ≤ b
source
theorem sub_mul_sub_pos_iff {R : Type u} [Ring R] [LinearOrder R] {a b : R} [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R] (x : R) (h : a ≤ b) :
0 < (x - a) * (x - b) ↔ x < a ∨ b < x
source
theorem sub_mul_sub_neg_iff {R : Type u} [Ring R] [LinearOrder R] {a b : R} [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R] (x : R) (h : a ≤ b) :
(x - a) * (x - b) < 0 ↔ a < x ∧ x < b