Ordered rings and semirings

This file develops the basics of ordered (semi)rings.

Each typeclass 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

• 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 <
  • Domain & linear order structure
• LinearOrderedCommRing
  • StrictOrderedCommRing & totality of the order
  • LinearOrderedRing & commutativity of multiplication
  • LinearOrderedCommSemiring & additive inverses
  • IsDomain & linear order structure

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

ink

theorem add_one_le_two_mul {α : Type u} [inst : LE α] [inst : Semiring α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} (a1 : 1 ≤ a) : a + 1 ≤ 2 * a

ink

class OrderedSemiring (α : Type u) extends Semiring , PartialOrder : Type u

• Addition is monotone in an OrderedAddCommMonoid.

  add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b

• 0 ≤ 1 in any ordered semiring.

  zero_le_one : 0 ≤ 1

• In an ordered semiring, we can multiply an inequality a ≤ b on the left by a non-negative element 0 ≤ c to obtain c * a ≤ c * b.

  mul_le_mul_of_nonneg_left : ∀ (a b c : α), a ≤ b → 0 ≤ c → c * a ≤ c * b

• In an ordered semiring, we can multiply an inequality a ≤ b on the right by a non-negative element 0 ≤ c to obtain a * c ≤ b * c.

  mul_le_mul_of_nonneg_right : ∀ (a b c : α), a ≤ b → 0 ≤ c → a * c ≤ b * c

An OrderedSemiring is a semiring with a partial order such that addition is monotone and multiplication by a nonnegative number is monotone.

ink

class OrderedCommSemiring (α : Type u) extends OrderedSemiring : Type u

• Multiplication is commutative in a commutative semigroup.

  mul_comm : ∀ (a b : α), a * b = b * a

An OrderedCommSemiring is a commutative semiring with a partial order such that addition is monotone and multiplication by a nonnegative number is monotone.

ink

class OrderedRing (α : Type u) extends Ring , PartialOrder : Type u

• Addition is monotone in a ordered additive commutative group.

  add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b

• 0 ≤ 1 in any ordered ring.

  zero_le_one : 0 ≤ 1

• The product of non-negative elements is non-negative.

  mul_nonneg : ∀ (a b : α), 0 ≤ a → 0 ≤ b → 0 ≤ a * b

An OrderedRing is a ring with a partial order such that addition is monotone and multiplication by a nonnegative number is monotone.

ink

class OrderedCommRing (α : Type u) extends OrderedRing : Type u

• Multiplication is commutative in a commutative semigroup.

  mul_comm : ∀ (a b : α), a * b = b * a

An OrderedCommRing is a commutative ring with a partial order such that addition is monotone and multiplication by a nonnegative number is monotone.

ink

class StrictOrderedSemiring (α : Type u) extends Semiring , PartialOrder , Nontrivial : Type u

• Additive cancellation is compatible with the order in an ordered cancellative additive commutative monoid.

  le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
• toNontrivial : Nontrivial α

• In a strict ordered semiring, 0 ≤ 1.

  zero_le_one : 0 ≤ 1

• Left multiplication by a positive element is strictly monotone.

  mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b → 0 < c → c * a < c * b

• Right multiplication by a positive element is strictly monotone.

  mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b → 0 < c → a * c < b * c

A StrictOrderedSemiring is a nontrivial semiring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.

ink

class StrictOrderedCommSemiring (α : Type u) extends StrictOrderedSemiring : Type u

• Multiplication is commutative in a commutative semigroup.

  mul_comm : ∀ (a b : α), a * b = b * a

A StrictOrderedCommSemiring is a commutative semiring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.

ink

class StrictOrderedRing (α : Type u) extends Ring , PartialOrder , Nontrivial : Type u

• toNontrivial : Nontrivial α

• In a strict ordered ring, 0 ≤ 1.

  zero_le_one : 0 ≤ 1

• The product of two positive elements is positive.

  mul_pos : ∀ (a b : α), 0 < a → 0 < b → 0 < a * b

A StrictOrderedRing is a ring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.

ink

class StrictOrderedCommRing (α : Type u_1) extends StrictOrderedRing : Type u_1

• Multiplication is commutative in a commutative semigroup.

  mul_comm : ∀ (a b : α), a * b = b * a

A StrictOrderedCommRing is a commutative ring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.

ink

class LinearOrderedSemiring (α : Type u) extends StrictOrderedSemiring , Min , Max , Ord : Type u

• A linear order is total.

  le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_le : DecidableRel fun x x_1 => x ≤ x_1

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_eq : DecidableEq α

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_lt : DecidableRel fun x x_1 => x < x_1

• The minimum function is equivalent to the one you get from minOfLe.

  min_def : autoParam (∀ (a b : α), min a b = if a ≤ b then a else b) _auto✝

• The minimum function is equivalent to the one you get from maxOfLe.

  max_def : autoParam (∀ (a b : α), max a b = if a ≤ b then b else a) _auto✝

• Comparison via compare is equal to the canonical comparison given decidable < and =.

  compare_eq_compareOfLessAndEq : autoParam (∀ (a b : α), compare a b = compareOfLessAndEq a b) _auto✝

A LinearOrderedSemiring is a nontrivial semiring with a linear order such that addition is monotone and multiplication by a positive number is strictly monotone.

ink

class LinearOrderedCommSemiring (α : Type u_1) extends StrictOrderedCommSemiring , Min , Max , Ord : Type u_1

• A linear order is total.

  le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_le : DecidableRel fun x x_1 => x ≤ x_1

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_eq : DecidableEq α

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_lt : DecidableRel fun x x_1 => x < x_1

• The minimum function is equivalent to the one you get from minOfLe.

  min_def : autoParam (∀ (a b : α), min a b = if a ≤ b then a else b) _auto✝

• The minimum function is equivalent to the one you get from maxOfLe.

  max_def : autoParam (∀ (a b : α), max a b = if a ≤ b then b else a) _auto✝

• Comparison via compare is equal to the canonical comparison given decidable < and =.

  compare_eq_compareOfLessAndEq : autoParam (∀ (a b : α), compare a b = compareOfLessAndEq a b) _auto✝

A LinearOrderedCommSemiring is a nontrivial commutative semiring with a linear order such that addition is monotone and multiplication by a positive number is strictly monotone.

ink

class LinearOrderedRing (α : Type u) extends StrictOrderedRing , Min , Max , Ord : Type u

• A linear order is total.

  le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_le : DecidableRel fun x x_1 => x ≤ x_1

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_eq : DecidableEq α

• In a linearly ordered type, we assume the order relations are all decidable.

  decidable_lt : DecidableRel fun x x_1 => x < x_1

• The minimum function is equivalent to the one you get from minOfLe.

  min_def : autoParam (∀ (a b : α), min a b = if a ≤ b then a else b) _auto✝

• The minimum function is equivalent to the one you get from maxOfLe.

  max_def : autoParam (∀ (a b : α), max a b = if a ≤ b then b else a) _auto✝

• Comparison via compare is equal to the canonical comparison given decidable < and =.

  compare_eq_compareOfLessAndEq : autoParam (∀ (a b : α), compare a b = compareOfLessAndEq a b) _auto✝

A LinearOrderedRing is a ring with a linear order such that addition is monotone and multiplication by a positive number is strictly monotone.

ink

class LinearOrderedCommRing (α : Type u) extends LinearOrderedRing : Type u

• Multiplication is commutative in a commutative semigroup.

  mul_comm : ∀ (a b : α), a * b = b * a

A LinearOrderedCommRing is a commutative ring with a linear order such that addition is monotone and multiplication by a positive number is strictly monotone.

ink

instance OrderedSemiring.zeroLEOneClass {α : Type u} [inst : OrderedSemiring α] : ZeroLEOneClass α

Equations

• OrderedSemiring.zeroLEOneClass = let src := inst; { zero_le_one := (_ : 0 ≤ 1) }

ink

instance OrderedSemiring.toPosMulMono {α : Type u} [inst : OrderedSemiring α] : PosMulMono α

Equations

• @OrderedSemiring.toPosMulMono = @OrderedSemiring.toPosMulMono.proof_1

ink

instance OrderedSemiring.toMulPosMono {α : Type u} [inst : OrderedSemiring α] : MulPosMono α

Equations

• @OrderedSemiring.toMulPosMono = @OrderedSemiring.toMulPosMono.proof_1

ink

theorem bit1_mono {α : Type u} [inst : OrderedSemiring α] : Monotone bit1

ink

@[simp]

theorem pow_nonneg {α : Type u} [inst : OrderedSemiring α] {a : α} (H : 0 ≤ a) (n : ℕ) : 0 ≤ a ^ n

ink

theorem add_le_mul_two_add {α : Type u} [inst : OrderedSemiring α] {a : α} {b : α} (a2 : 2 ≤ a) (b0 : 0 ≤ b) : a + (2 + b) ≤ a * (2 + b)

ink

theorem one_le_mul_of_one_le_of_one_le {α : Type u} [inst : OrderedSemiring α] {a : α} {b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b

ink

theorem monotone_mul_left_of_nonneg {α : Type u} [inst : OrderedSemiring α] {a : α} (ha : 0 ≤ a) : Monotone fun x => a * x

ink

theorem monotone_mul_right_of_nonneg {α : Type u} [inst : OrderedSemiring α] {a : α} (ha : 0 ≤ a) : Monotone fun x => x * a

ink

theorem Monotone.mul_const {α : Type u} {β : Type u_1} [inst : OrderedSemiring α] {a : α} [inst : Preorder β] {f : β → α} (hf : Monotone f) (ha : 0 ≤ a) : Monotone fun x => f x * a

ink

theorem Monotone.const_mul {α : Type u} {β : Type u_1} [inst : OrderedSemiring α] {a : α} [inst : Preorder β] {f : β → α} (hf : Monotone f) (ha : 0 ≤ a) : Monotone fun x => a * f x

ink

theorem Antitone.mul_const {α : Type u} {β : Type u_1} [inst : OrderedSemiring α] {a : α} [inst : Preorder β] {f : β → α} (hf : Antitone f) (ha : 0 ≤ a) : Antitone fun x => f x * a

ink

theorem Antitone.const_mul {α : Type u} {β : Type u_1} [inst : OrderedSemiring α] {a : α} [inst : Preorder β] {f : β → α} (hf : Antitone f) (ha : 0 ≤ a) : Antitone fun x => a * f x

ink

theorem Monotone.mul {α : Type u} {β : Type u_1} [inst : OrderedSemiring α] [inst : Preorder β] {f : β → α} {g : β → α} (hf : Monotone f) (hg : Monotone g) (hf₀ : ∀ (x : β), 0 ≤ f x) (hg₀ : ∀ (x : β), 0 ≤ g x) : Monotone (f * g)

ink

theorem bit1_pos {α : Type u} [inst : OrderedSemiring α] {a : α} [inst : Nontrivial α] (h : 0 ≤ a) : 0 < bit1 a

ink

theorem bit1_pos' {α : Type u} [inst : OrderedSemiring α] {a : α} (h : 0 < a) : 0 < bit1 a

ink

theorem mul_le_one {α : Type u} [inst : OrderedSemiring α] {a : α} {b : α} (ha : a ≤ 1) (hb' : 0 ≤ b) (hb : b ≤ 1) : a * b ≤ 1

ink

theorem one_lt_mul_of_le_of_lt {α : Type u} [inst : OrderedSemiring α] {a : α} {b : α} (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b

ink

theorem one_lt_mul_of_lt_of_le {α : Type u} [inst : OrderedSemiring α] {a : α} {b : α} (ha : 1 < a) (hb : 1 ≤ b) : 1 < a * b

ink

theorem one_lt_mul {α : Type u} [inst : OrderedSemiring α] {a : α} {b : α} (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b

Alias of one_lt_mul_of_le_of_lt.

ink

theorem mul_lt_one_of_nonneg_of_lt_one_left {α : Type u} [inst : OrderedSemiring α] {a : α} {b : α} (ha₀ : 0 ≤ a) (ha : a < 1) (hb : b ≤ 1) : a * b < 1

ink

theorem mul_lt_one_of_nonneg_of_lt_one_right {α : Type u} [inst : OrderedSemiring α] {a : α} {b : α} (ha : a ≤ 1) (hb₀ : 0 ≤ b) (hb : b < 1) : a * b < 1

ink

instance OrderedRing.toOrderedSemiring {α : Type u} [inst : OrderedRing α] : OrderedSemiring α

Equations

• One or more equations did not get rendered due to their size.

ink

theorem mul_le_mul_of_nonpos_left {α : Type u} [inst : OrderedRing α] {a : α} {b : α} {c : α} (h : b ≤ a) (hc : c ≤ 0) : c * a ≤ c * b

ink

theorem mul_le_mul_of_nonpos_right {α : Type u} [inst : OrderedRing α] {a : α} {b : α} {c : α} (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c

ink

theorem mul_nonneg_of_nonpos_of_nonpos {α : Type u} [inst : OrderedRing α] {a : α} {b : α} (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b

ink

theorem mul_le_mul_of_nonneg_of_nonpos {α : Type u} [inst : OrderedRing α] {a : α} {b : α} {c : α} {d : α} (hca : c ≤ a) (hbd : b ≤ d) (hc : 0 ≤ c) (hb : b ≤ 0) : a * b ≤ c * d

ink

theorem mul_le_mul_of_nonneg_of_nonpos' {α : Type u} [inst : OrderedRing α] {a : α} {b : α} {c : α} {d : α} (hca : c ≤ a) (hbd : b ≤ d) (ha : 0 ≤ a) (hd : d ≤ 0) : a * b ≤ c * d

ink

theorem mul_le_mul_of_nonpos_of_nonneg {α : Type u} [inst : OrderedRing α] {a : α} {b : α} {c : α} {d : α} (hac : a ≤ c) (hdb : d ≤ b) (hc : c ≤ 0) (hb : 0 ≤ b) : a * b ≤ c * d

ink

theorem mul_le_mul_of_nonpos_of_nonneg' {α : Type u} [inst : OrderedRing α] {a : α} {b : α} {c : α} {d : α} (hca : c ≤ a) (hbd : b ≤ d) (ha : 0 ≤ a) (hd : d ≤ 0) : a * b ≤ c * d

ink

theorem mul_le_mul_of_nonpos_of_nonpos {α : Type u} [inst : OrderedRing α] {a : α} {b : α} {c : α} {d : α} (hca : c ≤ a) (hdb : d ≤ b) (hc : c ≤ 0) (hb : b ≤ 0) : a * b ≤ c * d

ink

theorem mul_le_mul_of_nonpos_of_nonpos' {α : Type u} [inst : OrderedRing α] {a : α} {b : α} {c : α} {d : α} (hca : c ≤ a) (hdb : d ≤ b) (ha : a ≤ 0) (hd : d ≤ 0) : a * b ≤ c * d

ink

theorem antitone_mul_left {α : Type u} [inst : OrderedRing α] {a : α} (ha : a ≤ 0) : Antitone ((fun x x_1 => x * x_1) a)

ink

theorem antitone_mul_right {α : Type u} [inst : OrderedRing α] {a : α} (ha : a ≤ 0) : Antitone fun x => x * a

ink

theorem Monotone.const_mul_of_nonpos {α : Type u} {β : Type u_1} [inst : OrderedRing α] {a : α} [inst : Preorder β] {f : β → α} (hf : Monotone f) (ha : a ≤ 0) : Antitone fun x => a * f x

ink

theorem Monotone.mul_const_of_nonpos {α : Type u} {β : Type u_1} [inst : OrderedRing α] {a : α} [inst : Preorder β] {f : β → α} (hf : Monotone f) (ha : a ≤ 0) : Antitone fun x => f x * a

ink

theorem Antitone.const_mul_of_nonpos {α : Type u} {β : Type u_1} [inst : OrderedRing α] {a : α} [inst : Preorder β] {f : β → α} (hf : Antitone f) (ha : a ≤ 0) : Monotone fun x => a * f x

ink

theorem Antitone.mul_const_of_nonpos {α : Type u} {β : Type u_1} [inst : OrderedRing α] {a : α} [inst : Preorder β] {f : β → α} (hf : Antitone f) (ha : a ≤ 0) : Monotone fun x => f x * a

ink

theorem Antitone.mul_monotone {α : Type u} {β : Type u_1} [inst : OrderedRing α] [inst : Preorder β] {f : β → α} {g : β → α} (hf : Antitone f) (hg : Monotone g) (hf₀ : ∀ (x : β), f x ≤ 0) (hg₀ : ∀ (x : β), 0 ≤ g x) : Antitone (f * g)

ink

theorem Monotone.mul_antitone {α : Type u} {β : Type u_1} [inst : OrderedRing α] [inst : Preorder β] {f : β → α} {g : β → α} (hf : Monotone f) (hg : Antitone g) (hf₀ : ∀ (x : β), 0 ≤ f x) (hg₀ : ∀ (x : β), g x ≤ 0) : Antitone (f * g)

ink

theorem Antitone.mul {α : Type u} {β : Type u_1} [inst : OrderedRing α] [inst : Preorder β] {f : β → α} {g : β → α} (hf : Antitone f) (hg : Antitone g) (hf₀ : ∀ (x : β), f x ≤ 0) (hg₀ : ∀ (x : β), g x ≤ 0) : Monotone (f * g)

ink

theorem le_iff_exists_nonneg_add {α : Type u} [inst : OrderedRing α] (a : α) (b : α) : a ≤ b ↔ ∃ c, c ≥ 0 ∧ b = a + c

ink

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

Equations

• OrderedCommRing.toOrderedCommSemiring = let src := OrderedRing.toOrderedSemiring; let src_1 := inst; OrderedCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)

ink

instance StrictOrderedSemiring.toPosMulStrictMono {α : Type u} [inst : StrictOrderedSemiring α] : PosMulStrictMono α

Equations

• @StrictOrderedSemiring.toPosMulStrictMono = @StrictOrderedSemiring.toPosMulStrictMono.proof_1

ink

instance StrictOrderedSemiring.toMulPosStrictMono {α : Type u} [inst : StrictOrderedSemiring α] : MulPosStrictMono α

Equations

• @StrictOrderedSemiring.toMulPosStrictMono = @StrictOrderedSemiring.toMulPosStrictMono.proof_1

ink

def StrictOrderedSemiring.toOrderedSemiring' {α : Type u} [inst : StrictOrderedSemiring α] [inst : DecidableRel fun x x_1 => x ≤ x_1] : OrderedSemiring α

A choice-free version of StrictOrderedSemiring.toOrderedSemiring to avoid using choice in basic Nat lemmas.

Equations

• One or more equations did not get rendered due to their size.

ink

instance StrictOrderedSemiring.toOrderedSemiring {α : Type u} [inst : StrictOrderedSemiring α] : OrderedSemiring α

Equations

• One or more equations did not get rendered due to their size.

ink

theorem mul_lt_mul {α : Type u} [inst : StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} (hac : a < c) (hbd : b ≤ d) (hb : 0 < b) (hc : 0 ≤ c) : a * b < c * d

ink

theorem mul_lt_mul' {α : Type u} [inst : StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} (hac : a ≤ c) (hbd : b < d) (hb : 0 ≤ b) (hc : 0 < c) : a * b < c * d

ink

@[simp]

theorem pow_pos {α : Type u} [inst : StrictOrderedSemiring α] {a : α} (H : 0 < a) (n : ℕ) : 0 < a ^ n

ink

theorem mul_self_lt_mul_self {α : Type u} [inst : StrictOrderedSemiring α] {a : α} {b : α} (h1 : 0 ≤ a) (h2 : a < b) : a * a < b * b

ink

theorem strictMonoOn_mul_self {α : Type u} [inst : StrictOrderedSemiring α] : StrictMonoOn (fun x => x * x) { x | 0 ≤ x }

ink

theorem Decidable.mul_lt_mul'' {α : Type u} [inst : StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [inst : DecidableRel fun x x_1 => x ≤ x_1] (h1 : a < c) (h2 : b < d) (h3 : 0 ≤ a) (h4 : 0 ≤ b) : a * b < c * d

ink

theorem mul_lt_mul'' {α : Type u} [inst : StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} : a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d

ink

theorem lt_mul_left {α : Type u} [inst : StrictOrderedSemiring α] {a : α} {b : α} (hn : 0 < a) (hm : 1 < b) : a < b * a

ink

theorem lt_mul_right {α : Type u} [inst : StrictOrderedSemiring α] {a : α} {b : α} (hn : 0 < a) (hm : 1 < b) : a < a * b

ink

theorem lt_mul_self {α : Type u} [inst : StrictOrderedSemiring α] {a : α} (hn : 1 < a) : a < a * a

ink

theorem strictMono_mul_left_of_pos {α : Type u} [inst : StrictOrderedSemiring α] {a : α} (ha : 0 < a) : StrictMono fun x => a * x

ink

theorem strictMono_mul_right_of_pos {α : Type u} [inst : StrictOrderedSemiring α] {a : α} (ha : 0 < a) : StrictMono fun x => x * a

ink

theorem StrictMono.mul_const {α : Type u} {β : Type u_1} [inst : StrictOrderedSemiring α] {a : α} [inst : Preorder β] {f : β → α} (hf : StrictMono f) (ha : 0 < a) : StrictMono fun x => f x * a

ink

theorem StrictMono.const_mul {α : Type u} {β : Type u_1} [inst : StrictOrderedSemiring α] {a : α} [inst : Preorder β] {f : β → α} (hf : StrictMono f) (ha : 0 < a) : StrictMono fun x => a * f x

ink

theorem StrictAnti.mul_const {α : Type u} {β : Type u_1} [inst : StrictOrderedSemiring α] {a : α} [inst : Preorder β] {f : β → α} (hf : StrictAnti f) (ha : 0 < a) : StrictAnti fun x => f x * a

ink

theorem StrictAnti.const_mul {α : Type u} {β : Type u_1} [inst : StrictOrderedSemiring α] {a : α} [inst : Preorder β] {f : β → α} (hf : StrictAnti f) (ha : 0 < a) : StrictAnti fun x => a * f x

ink

theorem StrictMono.mul_monotone {α : Type u} {β : Type u_1} [inst : StrictOrderedSemiring α] [inst : Preorder β] {f : β → α} {g : β → α} (hf : StrictMono f) (hg : Monotone g) (hf₀ : ∀ (x : β), 0 ≤ f x) (hg₀ : ∀ (x : β), 0 < g x) : StrictMono (f * g)

ink

theorem Monotone.mul_strictMono {α : Type u} {β : Type u_1} [inst : StrictOrderedSemiring α] [inst : Preorder β] {f : β → α} {g : β → α} (hf : Monotone f) (hg : StrictMono g) (hf₀ : ∀ (x : β), 0 < f x) (hg₀ : ∀ (x : β), 0 ≤ g x) : StrictMono (f * g)

ink

theorem StrictMono.mul {α : Type u} {β : Type u_1} [inst : StrictOrderedSemiring α] [inst : Preorder β] {f : β → α} {g : β → α} (hf : StrictMono f) (hg : StrictMono g) (hf₀ : ∀ (x : β), 0 ≤ f x) (hg₀ : ∀ (x : β), 0 ≤ g x) : StrictMono (f * g)

ink

theorem lt_two_mul_self {α : Type u} [inst : StrictOrderedSemiring α] {a : α} (ha : 0 < a) : a < 2 * a

ink

instance StrictOrderedSemiring.toNoMaxOrder {α : Type u} [inst : StrictOrderedSemiring α] : NoMaxOrder α

Equations

• @StrictOrderedSemiring.toNoMaxOrder = @StrictOrderedSemiring.toNoMaxOrder.proof_1

ink

def StrictOrderedCommSemiring.toOrderedCommSemiring' {α : Type u} [inst : StrictOrderedCommSemiring α] [inst : DecidableRel fun x x_1 => x ≤ x_1] : OrderedCommSemiring α

A choice-free version of StrictOrderedCommSemiring.toOrderedCommSemiring' to avoid using choice in basic Nat lemmas.

Equations

• StrictOrderedCommSemiring.toOrderedCommSemiring' = let src := inst; let src_1 := StrictOrderedSemiring.toOrderedSemiring'; OrderedCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)

ink

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

Equations

• StrictOrderedCommSemiring.toOrderedCommSemiring = let src := inst; let src_1 := StrictOrderedSemiring.toOrderedSemiring; OrderedCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)

ink

instance StrictOrderedRing.toStrictOrderedSemiring {α : Type u} [inst : StrictOrderedRing α] : StrictOrderedSemiring α

Equations

• One or more equations did not get rendered due to their size.

ink

def StrictOrderedRing.toOrderedRing' {α : Type u} [inst : StrictOrderedRing α] [inst : DecidableRel fun x x_1 => x ≤ x_1] : OrderedRing α

A choice-free version of StrictOrderedRing.toOrderedRing to avoid using choice in basic Int lemmas.

Equations

• One or more equations did not get rendered due to their size.

ink

instance StrictOrderedRing.toOrderedRing {α : Type u} [inst : StrictOrderedRing α] : OrderedRing α

Equations

• StrictOrderedRing.toOrderedRing = let src := inst; OrderedRing.mk (_ : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b) (_ : 0 ≤ 1) (_ : ∀ (a b : α), 0 ≤ a → 0 ≤ b → 0 ≤ a * b)

ink

theorem mul_lt_mul_of_neg_left {α : Type u} [inst : StrictOrderedRing α] {a : α} {b : α} {c : α} (h : b < a) (hc : c < 0) : c * a < c * b

ink

theorem mul_lt_mul_of_neg_right {α : Type u} [inst : StrictOrderedRing α] {a : α} {b : α} {c : α} (h : b < a) (hc : c < 0) : a * c < b * c

ink

theorem mul_pos_of_neg_of_neg {α : Type u} [inst : StrictOrderedRing α] {a : α} {b : α} (ha : a < 0) (hb : b < 0) : 0 < a * b

ink

theorem strictAnti_mul_left {α : Type u} [inst : StrictOrderedRing α] {a : α} (ha : a < 0) : StrictAnti ((fun x x_1 => x * x_1) a)

ink

theorem strictAnti_mul_right {α : Type u} [inst : StrictOrderedRing α] {a : α} (ha : a < 0) : StrictAnti fun x => x * a

ink

theorem StrictMono.const_mul_of_neg {α : Type u} {β : Type u_1} [inst : StrictOrderedRing α] {a : α} [inst : Preorder β] {f : β → α} (hf : StrictMono f) (ha : a < 0) : StrictAnti fun x => a * f x

ink

theorem StrictMono.mul_const_of_neg {α : Type u} {β : Type u_1} [inst : StrictOrderedRing α] {a : α} [inst : Preorder β] {f : β → α} (hf : StrictMono f) (ha : a < 0) : StrictAnti fun x => f x * a

ink

theorem StrictAnti.const_mul_of_neg {α : Type u} {β : Type u_1} [inst : StrictOrderedRing α] {a : α} [inst : Preorder β] {f : β → α} (hf : StrictAnti f) (ha : a < 0) : StrictMono fun x => a * f x

ink

theorem StrictAnti.mul_const_of_neg {α : Type u} {β : Type u_1} [inst : StrictOrderedRing α] {a : α} [inst : Preorder β] {f : β → α} (hf : StrictAnti f) (ha : a < 0) : StrictMono fun x => f x * a

ink

def StrictOrderedCommRing.toOrderedCommRing' {α : Type u} [inst : StrictOrderedCommRing α] [inst : DecidableRel fun x x_1 => x ≤ x_1] : OrderedCommRing α

A choice-free version of StrictOrderedCommRing.toOrderedCommRing to avoid using choice in basic Int lemmas.

Equations

• StrictOrderedCommRing.toOrderedCommRing' = let src := inst; let src_1 := StrictOrderedRing.toOrderedRing'; OrderedCommRing.mk (_ : ∀ (a b : α), a * b = b * a)

ink

instance StrictOrderedCommRing.toStrictOrderedCommSemiring {α : Type u} [inst : StrictOrderedCommRing α] : StrictOrderedCommSemiring α

Equations

• StrictOrderedCommRing.toStrictOrderedCommSemiring = let src := inst; let src_1 := StrictOrderedRing.toStrictOrderedSemiring; StrictOrderedCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)

ink

instance StrictOrderedCommRing.toOrderedCommRing {α : Type u} [inst : StrictOrderedCommRing α] : OrderedCommRing α

Equations

• StrictOrderedCommRing.toOrderedCommRing = let src := inst; let src_1 := StrictOrderedRing.toOrderedRing; OrderedCommRing.mk (_ : ∀ (a b : α), a * b = b * a)

ink

instance LinearOrderedSemiring.toPosMulReflectLT {α : Type u} [inst : LinearOrderedSemiring α] : PosMulReflectLT α

Equations

• @LinearOrderedSemiring.toPosMulReflectLT = @LinearOrderedSemiring.toPosMulReflectLT.proof_1

ink

instance LinearOrderedSemiring.toMulPosReflectLT {α : Type u} [inst : LinearOrderedSemiring α] : MulPosReflectLT α

Equations

• @LinearOrderedSemiring.toMulPosReflectLT = @LinearOrderedSemiring.toMulPosReflectLT.proof_1

ink

theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nnonneg {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (hab : 0 ≤ a * b) : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

ink

theorem nonneg_of_mul_nonneg_left {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (h : 0 ≤ a * b) (hb : 0 < b) : 0 ≤ a

ink

theorem nonneg_of_mul_nonneg_right {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (h : 0 ≤ a * b) (ha : 0 < a) : 0 ≤ b

ink

theorem neg_of_mul_neg_left {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (h : a * b < 0) (hb : 0 ≤ b) : a < 0

ink

theorem neg_of_mul_neg_right {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (h : a * b < 0) (ha : 0 ≤ a) : b < 0

ink

theorem nonpos_of_mul_nonpos_left {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (h : a * b ≤ 0) (hb : 0 < b) : a ≤ 0

ink

theorem nonpos_of_mul_nonpos_right {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (h : a * b ≤ 0) (ha : 0 < a) : b ≤ 0

ink

@[simp]

theorem zero_le_mul_left {α : Type u} [inst : LinearOrderedSemiring α] {b : α} {c : α} (h : 0 < c) : 0 ≤ c * b ↔ 0 ≤ b

ink

@[simp]

theorem zero_le_mul_right {α : Type u} [inst : LinearOrderedSemiring α] {b : α} {c : α} (h : 0 < c) : 0 ≤ b * c ↔ 0 ≤ b

ink

theorem add_le_mul_of_left_le_right {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (a2 : 2 ≤ a) (ab : a ≤ b) : a + b ≤ a * b

ink

theorem add_le_mul_of_right_le_left {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (b2 : 2 ≤ b) (ba : b ≤ a) : a + b ≤ a * b

ink

theorem add_le_mul {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (a2 : 2 ≤ a) (b2 : 2 ≤ b) : a + b ≤ a * b

ink

theorem add_le_mul' {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (a2 : 2 ≤ a) (b2 : 2 ≤ b) : a + b ≤ b * a

ink

@[simp]

theorem bit0_le_bit0 {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} : bit0 a ≤ bit0 b ↔ a ≤ b

ink

@[simp]

theorem bit0_lt_bit0 {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} : bit0 a < bit0 b ↔ a < b

ink

@[simp]

theorem bit1_le_bit1 {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} : bit1 a ≤ bit1 b ↔ a ≤ b

ink

@[simp]

theorem bit1_lt_bit1 {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} : bit1 a < bit1 b ↔ a < b

ink

@[simp]

theorem one_le_bit1 {α : Type u} [inst : LinearOrderedSemiring α] {a : α} : 1 ≤ bit1 a ↔ 0 ≤ a

ink

@[simp]

theorem one_lt_bit1 {α : Type u} [inst : LinearOrderedSemiring α] {a : α} : 1 < bit1 a ↔ 0 < a

ink

@[simp]

theorem zero_le_bit0 {α : Type u} [inst : LinearOrderedSemiring α] {a : α} : 0 ≤ bit0 a ↔ 0 ≤ a

ink

@[simp]

theorem zero_lt_bit0 {α : Type u} [inst : LinearOrderedSemiring α] {a : α} : 0 < bit0 a ↔ 0 < a

ink

theorem mul_nonneg_iff_right_nonneg_of_pos {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (ha : 0 < a) : 0 ≤ a * b ↔ 0 ≤ b

ink

theorem mul_nonneg_iff_left_nonneg_of_pos {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (hb : 0 < b) : 0 ≤ a * b ↔ 0 ≤ a

ink

theorem nonpos_of_mul_nonneg_left {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (h : 0 ≤ a * b) (hb : b < 0) : a ≤ 0

ink

theorem nonpos_of_mul_nonneg_right {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (h : 0 ≤ a * b) (ha : a < 0) : b ≤ 0

ink

@[simp]

theorem Units.inv_pos {α : Type u} [inst : LinearOrderedSemiring α] {u : αˣ} : 0 < ↑u⁻¹ ↔ 0 < ↑u

ink

@[simp]

theorem Units.inv_neg {α : Type u} [inst : LinearOrderedSemiring α] {u : αˣ} : ↑u⁻¹ < 0 ↔ ↑u < 0

ink

theorem cmp_mul_pos_left {α : Type u} [inst : LinearOrderedSemiring α] {a : α} (ha : 0 < a) (b : α) (c : α) : cmp (a * b) (a * c) = cmp b c

ink

theorem cmp_mul_pos_right {α : Type u} [inst : LinearOrderedSemiring α] {a : α} (ha : 0 < a) (b : α) (c : α) : cmp (b * a) (c * a) = cmp b c

ink

theorem mul_max_of_nonneg {α : Type u} [inst : LinearOrderedSemiring α] {a : α} (b : α) (c : α) (ha : 0 ≤ a) : a * max b c = max (a * b) (a * c)

ink

theorem mul_min_of_nonneg {α : Type u} [inst : LinearOrderedSemiring α] {a : α} (b : α) (c : α) (ha : 0 ≤ a) : a * min b c = min (a * b) (a * c)

ink

theorem max_mul_of_nonneg {α : Type u} [inst : LinearOrderedSemiring α] {c : α} (a : α) (b : α) (hc : 0 ≤ c) : max a b * c = max (a * c) (b * c)

ink

theorem min_mul_of_nonneg {α : Type u} [inst : LinearOrderedSemiring α] {c : α} (a : α) (b : α) (hc : 0 ≤ c) : min a b * c = min (a * c) (b * c)

ink

theorem le_of_mul_le_of_one_le {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} {c : α} (h : a * c ≤ b) (hb : 0 ≤ b) (hc : 1 ≤ c) : a ≤ b

ink

theorem nonneg_le_nonneg_of_sq_le_sq {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (hb : 0 ≤ b) (h : a * a ≤ b * b) : a ≤ b

ink

theorem mul_self_le_mul_self_iff {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a ≤ b ↔ a * a ≤ b * b

ink

theorem mul_self_lt_mul_self_iff {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a < b ↔ a * a < b * b

ink

theorem mul_self_inj {α : Type u} [inst : LinearOrderedSemiring α] {a : α} {b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a * a = b * b ↔ a = b

ink

instance LinearOrderedCommSemiring.toLinearOrderedCancelAddCommMonoid {α : Type u} [inst : LinearOrderedCommSemiring α] : LinearOrderedCancelAddCommMonoid α

Equations

• One or more equations did not get rendered due to their size.

ink

instance LinearOrderedRing.toLinearOrderedSemiring {α : Type u} [inst : LinearOrderedRing α] : LinearOrderedSemiring α

Equations

• One or more equations did not get rendered due to their size.

ink

instance LinearOrderedRing.toLinearOrderedAddCommGroup {α : Type u} [inst : LinearOrderedRing α] : LinearOrderedAddCommGroup α

Equations

• One or more equations did not get rendered due to their size.

ink

instance LinearOrderedRing.noZeroDivisors {α : Type u} [inst : LinearOrderedRing α] : NoZeroDivisors α

Equations

• @LinearOrderedRing.noZeroDivisors = @LinearOrderedRing.noZeroDivisors.proof_1

ink

instance LinearOrderedRing.isDomain {α : Type u} [inst : LinearOrderedRing α] : IsDomain α

Equations

• @LinearOrderedRing.isDomain = @LinearOrderedRing.isDomain.proof_1

ink

theorem mul_pos_iff {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

ink

theorem mul_neg_iff {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} : a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

ink

theorem mul_nonneg_iff {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

ink

theorem mul_nonneg_of_three {α : Type u} [inst : LinearOrderedRing α] (a : α) (b : α) (c : α) : 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a

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

ink

theorem mul_nonpos_iff {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} : a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

ink

theorem mul_self_nonneg {α : Type u} [inst : LinearOrderedRing α] (a : α) : 0 ≤ a * a

ink

@[simp]

theorem neg_le_self_iff {α : Type u} [inst : LinearOrderedRing α] {a : α} : -a ≤ a ↔ 0 ≤ a

ink

@[simp]

theorem neg_lt_self_iff {α : Type u} [inst : LinearOrderedRing α] {a : α} : -a < a ↔ 0 < a

ink

@[simp]

theorem le_neg_self_iff {α : Type u} [inst : LinearOrderedRing α] {a : α} : a ≤ -a ↔ a ≤ 0

ink

@[simp]

theorem lt_neg_self_iff {α : Type u} [inst : LinearOrderedRing α] {a : α} : a < -a ↔ a < 0

ink

theorem neg_one_lt_zero {α : Type u} [inst : LinearOrderedRing α] : -1 < 0

ink

@[simp]

theorem mul_le_mul_left_of_neg {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} {c : α} (h : c < 0) : c * a ≤ c * b ↔ b ≤ a

ink

@[simp]

theorem mul_le_mul_right_of_neg {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} {c : α} (h : c < 0) : a * c ≤ b * c ↔ b ≤ a

ink

@[simp]

theorem mul_lt_mul_left_of_neg {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} {c : α} (h : c < 0) : c * a < c * b ↔ b < a

ink

@[simp]

theorem mul_lt_mul_right_of_neg {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} {c : α} (h : c < 0) : a * c < b * c ↔ b < a

ink

theorem lt_of_mul_lt_mul_of_nonpos_left {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} {c : α} (h : c * a < c * b) (hc : c ≤ 0) : b < a

ink

theorem lt_of_mul_lt_mul_of_nonpos_right {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} {c : α} (h : a * c < b * c) (hc : c ≤ 0) : b < a

ink

theorem cmp_mul_neg_left {α : Type u} [inst : LinearOrderedRing α] {a : α} (ha : a < 0) (b : α) (c : α) : cmp (a * b) (a * c) = cmp c b

ink

theorem cmp_mul_neg_right {α : Type u} [inst : LinearOrderedRing α] {a : α} (ha : a < 0) (b : α) (c : α) : cmp (b * a) (c * a) = cmp c b

ink

theorem sub_one_lt {α : Type u} [inst : LinearOrderedRing α] (a : α) : a - 1 < a

ink

@[simp]

theorem mul_self_pos {α : Type u} [inst : LinearOrderedRing α] {a : α} : 0 < a * a ↔ a ≠ 0

ink

theorem mul_self_le_mul_self_of_le_of_neg_le {α : Type u} [inst : LinearOrderedRing α] {x : α} {y : α} (h₁ : x ≤ y) (h₂ : -x ≤ y) : x * x ≤ y * y

ink

theorem nonneg_of_mul_nonpos_left {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} (h : a * b ≤ 0) (hb : b < 0) : 0 ≤ a

ink

theorem nonneg_of_mul_nonpos_right {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} (h : a * b ≤ 0) (ha : a < 0) : 0 ≤ b

ink

theorem pos_of_mul_neg_left {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} (h : a * b < 0) (hb : b ≤ 0) : 0 < a

ink

theorem pos_of_mul_neg_right {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} (h : a * b < 0) (ha : a ≤ 0) : 0 < b

ink

theorem neg_iff_pos_of_mul_neg {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} (hab : a * b < 0) : a < 0 ↔ 0 < b

ink

theorem pos_iff_neg_of_mul_neg {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} (hab : a * b < 0) : 0 < a ↔ b < 0

ink

theorem mul_self_add_mul_self_eq_zero {α : Type u} [inst : LinearOrderedRing α] {x : α} {y : α} : x * x + y * y = 0 ↔ x = 0 ∧ y = 0

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

ink

theorem eq_zero_of_mul_self_add_mul_self_eq_zero {α : Type u} [inst : LinearOrderedRing α] {a : α} {b : α} (h : a * a + b * b = 0) : a = 0

ink

instance LinearOrderedCommRing.toStrictOrderedCommRing {α : Type u} [d : LinearOrderedCommRing α] : StrictOrderedCommRing α

Equations

• LinearOrderedCommRing.toStrictOrderedCommRing = StrictOrderedCommRing.mk (_ : ∀ (a b : α), a * b = b * a)

ink

instance LinearOrderedCommRing.toLinearOrderedCommSemiring {α : Type u} [d : LinearOrderedCommRing α] : LinearOrderedCommSemiring α

Equations

• One or more equations did not get rendered due to their size.

ink

theorem max_mul_mul_le_max_mul_max {α : Type u} [inst : LinearOrderedCommRing α] {a : α} {d : α} (b : α) (c : α) (ha : 0 ≤ a) (hd : 0 ≤ d) : max (a * b) (d * c) ≤ max a c * max d b