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.

theorem add_one_le_two_mul {R : Type u} [LE R] [NonAssocSemiring R] [AddLeftMono R] {a : R} (a1 : 1 ≤ a) : a + 1 ≤ 2 * a

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)

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

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

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

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

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

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

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

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

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

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.

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.

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.

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.

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

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

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

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

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

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

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)

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)

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)

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

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

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

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

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.

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.

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.

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.

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

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

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

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

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

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

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.

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.

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.

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.

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

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

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

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

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

@[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

@[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

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

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

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

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

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

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

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

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

@[simp]

theorem Units.inv_pos {R : Type u} [Semiring R] [LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [PosMulStrictMono R] {u : Rˣ} : 0 < ↑u⁻¹ ↔ 0 < ↑u

@[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

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

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

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)

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)

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)

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)

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

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

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

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

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

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

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

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

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.

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)

@[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

@[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

@[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

@[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

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

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

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

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

@[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

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

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

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

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

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

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

theorem sq_nonneg {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] (a : R) : 0 ≤ a ^ 2

@[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

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.

theorem mul_self_nonneg {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] (a : R) : 0 ≤ a * a

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.

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

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

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.

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.

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.

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.

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.

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

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

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)

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)

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)

theorem neg_one_lt_zero {R : Type u} [Ring R] [LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [AddLeftStrictMono R] : -1 < 0

theorem sub_one_lt {R : Type u} [Ring R] [LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [AddLeftStrictMono R] (a : R) : a - 1 < a

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

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

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

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

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