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 Algebra.Order.Ring.Defs.
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<, anda ≤ 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.
OrderedSemiringOrderedAddCommMonoid& multiplication &*respects≤Semiring& partial order structure &+respects≤&*respects≤
StrictOrderedSemiringOrderedCancelAddCommMonoid& multiplication &*respects<& nontrivialityOrderedSemiring&+respects<&*respects<& nontriviality
OrderedCommSemiringOrderedSemiring& commutativity of multiplicationCommSemiring& partial order structure &+respects≤&*respects<
StrictOrderedCommSemiringStrictOrderedSemiring& commutativity of multiplicationOrderedCommSemiring&+respects<&*respects<& nontriviality
OrderedRingOrderedSemiring& additive inversesOrderedAddCommGroup& multiplication &*respects<Ring& partial order structure &+respects≤&*respects<
StrictOrderedRingStrictOrderedSemiring& additive inversesOrderedSemiring&+respects<&*respects<& nontriviality
OrderedCommRingOrderedRing& commutativity of multiplicationOrderedCommSemiring& additive inversesCommRing& partial order structure &+respects≤&*respects<
StrictOrderedCommRingStrictOrderedCommSemiring& additive inversesStrictOrderedRing& commutativity of multiplicationOrderedCommRing&+respects<&*respects<& nontriviality
LinearOrderedSemiringStrictOrderedSemiring& totality of the orderLinearOrderedAddCommMonoid& multiplication & nontriviality &*respects<
LinearOrderedCommSemiringStrictOrderedCommSemiring& totality of the orderLinearOrderedSemiring& commutativity of multiplication
LinearOrderedRingLinearOrderedCommRing
Generality #
Each section is labelled with a corresponding bundled ordered ring typeclass in mind. Mixin's for relating the order structures and ring structures are added as needed.
TODO: the mixin assumptiosn 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_le_mul_two_add
{α : Type u}
[Semiring α]
[Preorder α]
{a : α}
{b : α}
[ZeroLEOneClass α]
[MulPosMono α]
[AddLeftMono α]
(a2 : 2 ≤ a)
(b0 : 0 ≤ b)
:
theorem
mul_le_mul_of_nonpos_left
{α : Type u}
[Semiring α]
[Preorder α]
{a : α}
{b : α}
{c : α}
[ExistsAddOfLE α]
[PosMulMono α]
[AddRightMono α]
[AddRightReflectLE α]
(h : b ≤ a)
(hc : c ≤ 0)
:
theorem
mul_le_mul_of_nonpos_right
{α : Type u}
[Semiring α]
[Preorder α]
{a : α}
{b : α}
{c : α}
[ExistsAddOfLE α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
(h : b ≤ a)
(hc : c ≤ 0)
:
theorem
mul_nonneg_of_nonpos_of_nonpos
{α : Type u}
[Semiring α]
[Preorder α]
{a : α}
{b : α}
[ExistsAddOfLE α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
(ha : a ≤ 0)
(hb : b ≤ 0)
:
theorem
mul_le_mul_of_nonneg_of_nonpos
{α : Type u}
[Semiring α]
[Preorder α]
{a : α}
{b : α}
{c : α}
{d : α}
[ExistsAddOfLE α]
[MulPosMono α]
[PosMulMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hca : c ≤ a)
(hbd : b ≤ d)
(hc : 0 ≤ c)
(hb : b ≤ 0)
:
theorem
mul_le_mul_of_nonneg_of_nonpos'
{α : Type u}
[Semiring α]
[Preorder α]
{a : α}
{b : α}
{c : α}
{d : α}
[ExistsAddOfLE α]
[PosMulMono α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hca : c ≤ a)
(hbd : b ≤ d)
(ha : 0 ≤ a)
(hd : d ≤ 0)
:
theorem
mul_le_mul_of_nonpos_of_nonneg
{α : Type u}
[Semiring α]
[Preorder α]
{a : α}
{b : α}
{c : α}
{d : α}
[ExistsAddOfLE α]
[MulPosMono α]
[PosMulMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hac : a ≤ c)
(hdb : d ≤ b)
(hc : c ≤ 0)
(hb : 0 ≤ b)
:
theorem
mul_le_mul_of_nonpos_of_nonneg'
{α : Type u}
[Semiring α]
[Preorder α]
{a : α}
{b : α}
{c : α}
{d : α}
[ExistsAddOfLE α]
[PosMulMono α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hca : c ≤ a)
(hbd : b ≤ d)
(ha : 0 ≤ a)
(hd : d ≤ 0)
:
theorem
mul_le_mul_of_nonpos_of_nonpos
{α : Type u}
[Semiring α]
[Preorder α]
{a : α}
{b : α}
{c : α}
{d : α}
[ExistsAddOfLE α]
[MulPosMono α]
[PosMulMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hca : c ≤ a)
(hdb : d ≤ b)
(hc : c ≤ 0)
(hb : b ≤ 0)
:
theorem
mul_le_mul_of_nonpos_of_nonpos'
{α : Type u}
[Semiring α]
[Preorder α]
{a : α}
{b : α}
{c : α}
{d : α}
[ExistsAddOfLE α]
[PosMulMono α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hca : c ≤ a)
(hdb : d ≤ b)
(ha : a ≤ 0)
(hd : d ≤ 0)
:
theorem
le_mul_of_le_one_left
{α : Type u}
[Semiring α]
[Preorder α]
{a : α}
{b : α}
[ExistsAddOfLE α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hb : b ≤ 0)
(h : a ≤ 1)
:
Variant of mul_le_of_le_one_left for b non-positive instead of non-negative.
theorem
mul_le_of_one_le_left
{α : Type u}
[Semiring α]
[Preorder α]
{a : α}
{b : α}
[ExistsAddOfLE α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hb : b ≤ 0)
(h : 1 ≤ a)
:
Variant of le_mul_of_one_le_left for b non-positive instead of non-negative.
theorem
le_mul_of_le_one_right
{α : Type u}
[Semiring α]
[Preorder α]
{a : α}
{b : α}
[ExistsAddOfLE α]
[PosMulMono α]
[AddRightMono α]
[AddRightReflectLE α]
(ha : a ≤ 0)
(h : b ≤ 1)
:
Variant of mul_le_of_le_one_right for a non-positive instead of non-negative.
theorem
mul_le_of_one_le_right
{α : Type u}
[Semiring α]
[Preorder α]
{a : α}
{b : α}
[ExistsAddOfLE α]
[PosMulMono α]
[AddRightMono α]
[AddRightReflectLE α]
(ha : a ≤ 0)
(h : 1 ≤ b)
:
Variant of le_mul_of_one_le_right for a non-positive instead of non-negative.
theorem
antitone_mul_left
{α : Type u}
[Semiring α]
[Preorder α]
[ExistsAddOfLE α]
[PosMulMono α]
[AddRightMono α]
[AddRightReflectLE α]
{a : α}
(ha : a ≤ 0)
:
theorem
antitone_mul_right
{α : Type u}
[Semiring α]
[Preorder α]
[ExistsAddOfLE α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
{a : α}
(ha : a ≤ 0)
:
theorem
Monotone.const_mul_of_nonpos
{α : Type u}
{β : Type u_1}
[Semiring α]
[Preorder α]
{a : α}
[Preorder β]
{f : β → α}
[ExistsAddOfLE α]
[PosMulMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hf : Monotone f)
(ha : a ≤ 0)
:
theorem
Monotone.mul_const_of_nonpos
{α : Type u}
{β : Type u_1}
[Semiring α]
[Preorder α]
{a : α}
[Preorder β]
{f : β → α}
[ExistsAddOfLE α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hf : Monotone f)
(ha : a ≤ 0)
:
theorem
Antitone.const_mul_of_nonpos
{α : Type u}
{β : Type u_1}
[Semiring α]
[Preorder α]
{a : α}
[Preorder β]
{f : β → α}
[ExistsAddOfLE α]
[PosMulMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hf : Antitone f)
(ha : a ≤ 0)
:
theorem
Antitone.mul_const_of_nonpos
{α : Type u}
{β : Type u_1}
[Semiring α]
[Preorder α]
{a : α}
[Preorder β]
{f : β → α}
[ExistsAddOfLE α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hf : Antitone f)
(ha : a ≤ 0)
:
theorem
Antitone.mul_monotone
{α : Type u}
{β : Type u_1}
[Semiring α]
[Preorder α]
[Preorder β]
{f : β → α}
{g : β → α}
[ExistsAddOfLE α]
[PosMulMono α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hf : Antitone f)
(hg : Monotone g)
(hf₀ : ∀ (x : β), f x ≤ 0)
(hg₀ : ∀ (x : β), 0 ≤ g x)
:
theorem
Monotone.mul_antitone
{α : Type u}
{β : Type u_1}
[Semiring α]
[Preorder α]
[Preorder β]
{f : β → α}
{g : β → α}
[ExistsAddOfLE α]
[PosMulMono α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hf : Monotone f)
(hg : Antitone g)
(hf₀ : ∀ (x : β), 0 ≤ f x)
(hg₀ : ∀ (x : β), g x ≤ 0)
:
theorem
Antitone.mul
{α : Type u}
{β : Type u_1}
[Semiring α]
[Preorder α]
[Preorder β]
{f : β → α}
{g : β → α}
[ExistsAddOfLE α]
[PosMulMono α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hf : Antitone f)
(hg : Antitone g)
(hf₀ : ∀ (x : β), f x ≤ 0)
(hg₀ : ∀ (x : β), g x ≤ 0)
:
theorem
lt_two_mul_self
{α : Type u}
[Semiring α]
[PartialOrder α]
{a : α}
[ZeroLEOneClass α]
[MulPosStrictMono α]
[NeZero 1]
[AddLeftStrictMono α]
(ha : 0 < a)
:
theorem
mul_lt_mul_of_neg_left
{α : Type u}
[Semiring α]
[PartialOrder α]
{a : α}
{b : α}
{c : α}
[ExistsAddOfLE α]
[PosMulStrictMono α]
[AddRightStrictMono α]
[AddRightReflectLT α]
(h : b < a)
(hc : c < 0)
:
theorem
mul_lt_mul_of_neg_right
{α : Type u}
[Semiring α]
[PartialOrder α]
{a : α}
{b : α}
{c : α}
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddRightStrictMono α]
[AddRightReflectLT α]
(h : b < a)
(hc : c < 0)
:
theorem
mul_pos_of_neg_of_neg
{α : Type u}
[Semiring α]
[PartialOrder α]
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddRightStrictMono α]
[AddRightReflectLT α]
{a : α}
{b : α}
(ha : a < 0)
(hb : b < 0)
:
theorem
lt_mul_of_lt_one_left
{α : Type u}
[Semiring α]
[PartialOrder α]
{a : α}
{b : α}
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddRightStrictMono α]
[AddRightReflectLT α]
(hb : b < 0)
(h : a < 1)
:
Variant of mul_lt_of_lt_one_left for b negative instead of positive.
theorem
mul_lt_of_one_lt_left
{α : Type u}
[Semiring α]
[PartialOrder α]
{a : α}
{b : α}
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddRightStrictMono α]
[AddRightReflectLT α]
(hb : b < 0)
(h : 1 < a)
:
Variant of lt_mul_of_one_lt_left for b negative instead of positive.
theorem
lt_mul_of_lt_one_right
{α : Type u}
[Semiring α]
[PartialOrder α]
{a : α}
{b : α}
[ExistsAddOfLE α]
[PosMulStrictMono α]
[AddRightStrictMono α]
[AddRightReflectLT α]
(ha : a < 0)
(h : b < 1)
:
Variant of mul_lt_of_lt_one_right for a negative instead of positive.
theorem
mul_lt_of_one_lt_right
{α : Type u}
[Semiring α]
[PartialOrder α]
{a : α}
{b : α}
[ExistsAddOfLE α]
[PosMulStrictMono α]
[AddRightStrictMono α]
[AddRightReflectLT α]
(ha : a < 0)
(h : 1 < b)
:
Variant of lt_mul_of_lt_one_right for a negative instead of positive.
theorem
strictAnti_mul_left
{α : Type u}
[Semiring α]
[PartialOrder α]
[ExistsAddOfLE α]
[PosMulStrictMono α]
[AddRightStrictMono α]
[AddRightReflectLT α]
{a : α}
(ha : a < 0)
:
StrictAnti fun (x : α) => a * x
theorem
strictAnti_mul_right
{α : Type u}
[Semiring α]
[PartialOrder α]
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddRightStrictMono α]
[AddRightReflectLT α]
{a : α}
(ha : a < 0)
:
StrictAnti fun (x : α) => x * a
theorem
StrictMono.const_mul_of_neg
{α : Type u}
{β : Type u_1}
[Semiring α]
[PartialOrder α]
{a : α}
[Preorder β]
{f : β → α}
[ExistsAddOfLE α]
[PosMulStrictMono α]
[AddRightStrictMono α]
[AddRightReflectLT α]
(hf : StrictMono f)
(ha : a < 0)
:
StrictAnti fun (x : β) => a * f x
theorem
StrictMono.mul_const_of_neg
{α : Type u}
{β : Type u_1}
[Semiring α]
[PartialOrder α]
{a : α}
[Preorder β]
{f : β → α}
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddRightStrictMono α]
[AddRightReflectLT α]
(hf : StrictMono f)
(ha : a < 0)
:
StrictAnti fun (x : β) => f x * a
theorem
StrictAnti.const_mul_of_neg
{α : Type u}
{β : Type u_1}
[Semiring α]
[PartialOrder α]
{a : α}
[Preorder β]
{f : β → α}
[ExistsAddOfLE α]
[PosMulStrictMono α]
[AddRightStrictMono α]
[AddRightReflectLT α]
(hf : StrictAnti f)
(ha : a < 0)
:
StrictMono fun (x : β) => a * f x
theorem
StrictAnti.mul_const_of_neg
{α : Type u}
{β : Type u_1}
[Semiring α]
[PartialOrder α]
{a : α}
[Preorder β]
{f : β → α}
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddRightStrictMono α]
[AddRightReflectLT α]
(hf : StrictAnti f)
(ha : a < 0)
:
StrictMono fun (x : β) => f x * a
theorem
mul_add_mul_le_mul_add_mul
{α : Type u}
[Semiring α]
[PartialOrder α]
{a : α}
{b : α}
{c : α}
{d : α}
[ExistsAddOfLE α]
[MulPosMono α]
[AddLeftMono α]
[AddLeftReflectLE α]
(hab : a ≤ b)
(hcd : c ≤ d)
:
Binary rearrangement inequality.
theorem
mul_add_mul_le_mul_add_mul'
{α : Type u}
[Semiring α]
[PartialOrder α]
{a : α}
{b : α}
{c : α}
{d : α}
[ExistsAddOfLE α]
[MulPosMono α]
[AddLeftMono α]
[AddLeftReflectLE α]
(hba : b ≤ a)
(hdc : d ≤ c)
:
Binary rearrangement inequality.
theorem
mul_add_mul_lt_mul_add_mul
{α : Type u}
[Semiring α]
[PartialOrder α]
{a : α}
{b : α}
{c : α}
{d : α}
[AddLeftReflectLT α]
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddLeftStrictMono α]
(hab : a < b)
(hcd : c < d)
:
Binary strict rearrangement inequality.
theorem
mul_add_mul_lt_mul_add_mul'
{α : Type u}
[Semiring α]
[PartialOrder α]
{a : α}
{b : α}
{c : α}
{d : α}
[AddLeftReflectLT α]
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddLeftStrictMono α]
(hba : b < a)
(hdc : d < c)
:
Binary rearrangement inequality.
theorem
nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[MulPosStrictMono α]
[PosMulStrictMono α]
(hab : 0 ≤ a * b)
:
theorem
nonneg_of_mul_nonneg_left
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[MulPosStrictMono α]
(h : 0 ≤ a * b)
(hb : 0 < b)
:
0 ≤ a
theorem
nonneg_of_mul_nonneg_right
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[PosMulStrictMono α]
(h : 0 ≤ a * b)
(ha : 0 < a)
:
0 ≤ b
theorem
nonpos_of_mul_nonpos_left
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[PosMulStrictMono α]
(h : a * b ≤ 0)
(hb : 0 < b)
:
a ≤ 0
theorem
nonpos_of_mul_nonpos_right
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[PosMulStrictMono α]
(h : a * b ≤ 0)
(ha : 0 < a)
:
b ≤ 0
@[simp]
theorem
mul_nonneg_iff_of_pos_left
{α : Type u}
[Semiring α]
[LinearOrder α]
{b : α}
{c : α}
[PosMulStrictMono α]
(h : 0 < c)
:
@[simp]
theorem
mul_nonneg_iff_of_pos_right
{α : Type u}
[Semiring α]
[LinearOrder α]
{b : α}
{c : α}
[MulPosStrictMono α]
(h : 0 < c)
:
theorem
add_le_mul_of_left_le_right
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[ZeroLEOneClass α]
[NeZero 1]
[MulPosStrictMono α]
[AddLeftMono α]
(a2 : 2 ≤ a)
(ab : a ≤ b)
:
theorem
add_le_mul_of_right_le_left
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[ZeroLEOneClass α]
[NeZero 1]
[AddLeftMono α]
[PosMulStrictMono α]
(b2 : 2 ≤ b)
(ba : b ≤ a)
:
theorem
add_le_mul
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[ZeroLEOneClass α]
[NeZero 1]
[MulPosStrictMono α]
[PosMulStrictMono α]
[AddLeftMono α]
(a2 : 2 ≤ a)
(b2 : 2 ≤ b)
:
theorem
add_le_mul'
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[ZeroLEOneClass α]
[NeZero 1]
[MulPosStrictMono α]
[PosMulStrictMono α]
[AddLeftMono α]
(a2 : 2 ≤ a)
(b2 : 2 ≤ b)
:
theorem
mul_nonneg_iff_right_nonneg_of_pos
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[PosMulStrictMono α]
(ha : 0 < a)
:
theorem
mul_nonneg_iff_left_nonneg_of_pos
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[PosMulStrictMono α]
[MulPosStrictMono α]
(hb : 0 < b)
:
theorem
nonpos_of_mul_nonneg_left
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[PosMulStrictMono α]
(h : 0 ≤ a * b)
(hb : b < 0)
:
a ≤ 0
theorem
nonpos_of_mul_nonneg_right
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[MulPosStrictMono α]
(h : 0 ≤ a * b)
(ha : a < 0)
:
b ≤ 0
@[simp]
theorem
Units.inv_pos
{α : Type u}
[Semiring α]
[LinearOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[PosMulStrictMono α]
{u : αˣ}
:
@[simp]
theorem
Units.inv_neg
{α : Type u}
[Semiring α]
[LinearOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[MulPosMono α]
[PosMulMono α]
{u : αˣ}
:
theorem
cmp_mul_pos_left
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
[PosMulStrictMono α]
(ha : 0 < a)
(b : α)
(c : α)
:
theorem
cmp_mul_pos_right
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
[MulPosStrictMono α]
(ha : 0 < a)
(b : α)
(c : α)
:
theorem
mul_max_of_nonneg
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
[PosMulMono α]
(b : α)
(c : α)
(ha : 0 ≤ a)
:
theorem
mul_min_of_nonneg
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
[PosMulMono α]
(b : α)
(c : α)
(ha : 0 ≤ a)
:
theorem
max_mul_of_nonneg
{α : Type u}
[Semiring α]
[LinearOrder α]
{c : α}
[MulPosMono α]
(a : α)
(b : α)
(hc : 0 ≤ c)
:
theorem
min_mul_of_nonneg
{α : Type u}
[Semiring α]
[LinearOrder α]
{c : α}
[MulPosMono α]
(a : α)
(b : α)
(hc : 0 ≤ c)
:
theorem
le_of_mul_le_of_one_le
{α : Type u}
[Semiring α]
[LinearOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[MulPosStrictMono α]
[PosMulMono α]
{a : α}
{b : α}
{c : α}
(h : a * c ≤ b)
(hb : 0 ≤ b)
(hc : 1 ≤ c)
:
a ≤ b
theorem
nonneg_le_nonneg_of_sq_le_sq
{α : Type u}
[Semiring α]
[LinearOrder α]
[PosMulStrictMono α]
[MulPosMono α]
{a : α}
{b : α}
(hb : 0 ≤ b)
(h : a * a ≤ b * b)
:
a ≤ b
theorem
mul_self_le_mul_self_iff
{α : Type u}
[Semiring α]
[LinearOrder α]
[PosMulStrictMono α]
[MulPosMono α]
{a : α}
{b : α}
(h1 : 0 ≤ a)
(h2 : 0 ≤ b)
:
theorem
mul_self_lt_mul_self_iff
{α : Type u}
[Semiring α]
[LinearOrder α]
[PosMulStrictMono α]
[MulPosMono α]
{a : α}
{b : α}
(h1 : 0 ≤ a)
(h2 : 0 ≤ b)
:
theorem
mul_self_inj
{α : Type u}
[Semiring α]
[LinearOrder α]
[PosMulStrictMono α]
[MulPosMono α]
{a : α}
{b : α}
(h1 : 0 ≤ a)
(h2 : 0 ≤ b)
:
theorem
sign_cases_of_C_mul_pow_nonneg
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[PosMulStrictMono α]
(h : ∀ (n : ℕ), 0 ≤ a * b ^ n)
:
theorem
mul_pos_iff
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[ExistsAddOfLE α]
[PosMulStrictMono α]
[MulPosStrictMono α]
[AddLeftStrictMono α]
[AddLeftReflectLT α]
:
theorem
mul_nonneg_iff
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[ExistsAddOfLE α]
[MulPosStrictMono α]
[PosMulStrictMono α]
[AddLeftReflectLE α]
[AddLeftMono α]
:
theorem
mul_nonneg_of_three
{α : Type u}
[Semiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[MulPosStrictMono α]
[PosMulStrictMono α]
[AddLeftMono α]
[AddLeftReflectLE α]
(a : α)
(b : α)
(c : α)
:
Out of three elements of a LinearOrderedRing, two must have the same sign.
theorem
mul_nonneg_iff_pos_imp_nonneg
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[ExistsAddOfLE α]
[PosMulStrictMono α]
[MulPosStrictMono α]
[AddLeftMono α]
[AddLeftReflectLE α]
:
@[simp]
theorem
mul_le_mul_left_of_neg
{α : Type u}
[Semiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[PosMulStrictMono α]
[AddRightMono α]
[AddRightReflectLE α]
{a : α}
{b : α}
{c : α}
(h : c < 0)
:
@[simp]
theorem
mul_le_mul_right_of_neg
{α : Type u}
[Semiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddRightMono α]
[AddRightReflectLE α]
{a : α}
{b : α}
{c : α}
(h : c < 0)
:
@[simp]
theorem
mul_lt_mul_left_of_neg
{α : Type u}
[Semiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[PosMulStrictMono α]
[AddRightStrictMono α]
[AddRightReflectLT α]
{a : α}
{b : α}
{c : α}
(h : c < 0)
:
@[simp]
theorem
mul_lt_mul_right_of_neg
{α : Type u}
[Semiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddRightStrictMono α]
[AddRightReflectLT α]
{a : α}
{b : α}
{c : α}
(h : c < 0)
:
theorem
lt_of_mul_lt_mul_of_nonpos_left
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
{c : α}
[ExistsAddOfLE α]
[PosMulMono α]
[AddRightMono α]
[AddRightReflectLE α]
(h : c * a < c * b)
(hc : c ≤ 0)
:
b < a
theorem
lt_of_mul_lt_mul_of_nonpos_right
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
{c : α}
[ExistsAddOfLE α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
(h : a * c < b * c)
(hc : c ≤ 0)
:
b < a
theorem
cmp_mul_neg_left
{α : Type u}
[Semiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[PosMulStrictMono α]
[AddRightReflectLT α]
[AddRightStrictMono α]
{a : α}
(ha : a < 0)
(b : α)
(c : α)
:
theorem
cmp_mul_neg_right
{α : Type u}
[Semiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddRightReflectLT α]
[AddRightStrictMono α]
{a : α}
(ha : a < 0)
(b : α)
(c : α)
:
@[simp]
theorem
mul_self_pos
{α : Type u}
[Semiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[PosMulStrictMono α]
[MulPosStrictMono α]
[AddLeftStrictMono α]
[AddLeftReflectLT α]
{a : α}
:
theorem
nonneg_of_mul_nonpos_left
{α : Type u}
[Semiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddRightMono α]
[AddRightReflectLE α]
{a : α}
{b : α}
(h : a * b ≤ 0)
(hb : b < 0)
:
0 ≤ a
theorem
nonneg_of_mul_nonpos_right
{α : Type u}
[Semiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddRightMono α]
[AddRightReflectLE α]
{a : α}
{b : α}
(h : a * b ≤ 0)
(ha : a < 0)
:
0 ≤ b
theorem
pos_of_mul_neg_left
{α : Type u}
[Semiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
{a : α}
{b : α}
(h : a * b < 0)
(hb : b ≤ 0)
:
0 < a
theorem
pos_of_mul_neg_right
{α : Type u}
[Semiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
{a : α}
{b : α}
(h : a * b < 0)
(ha : a ≤ 0)
:
0 < b
theorem
neg_iff_pos_of_mul_neg
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[ExistsAddOfLE α]
[PosMulMono α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hab : a * b < 0)
:
theorem
pos_iff_neg_of_mul_neg
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[ExistsAddOfLE α]
[PosMulMono α]
[MulPosMono α]
[AddRightMono α]
[AddRightReflectLE α]
(hab : a * b < 0)
:
theorem
sq_nonneg
{α : Type u}
[Semiring α]
[LinearOrder α]
[IsRightCancelAdd α]
[ZeroLEOneClass α]
[ExistsAddOfLE α]
[PosMulMono α]
[AddLeftStrictMono α]
(a : α)
:
theorem
pow_two_nonneg
{α : Type u}
[Semiring α]
[LinearOrder α]
[IsRightCancelAdd α]
[ZeroLEOneClass α]
[ExistsAddOfLE α]
[PosMulMono α]
[AddLeftStrictMono α]
(a : α)
:
Alias of sq_nonneg.
theorem
mul_self_nonneg
{α : Type u}
[Semiring α]
[LinearOrder α]
[IsRightCancelAdd α]
[ZeroLEOneClass α]
[ExistsAddOfLE α]
[PosMulMono α]
[AddLeftStrictMono α]
(a : α)
:
theorem
mul_self_add_mul_self_eq_zero
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[IsRightCancelAdd α]
[NoZeroDivisors α]
[ZeroLEOneClass α]
[ExistsAddOfLE α]
[PosMulMono α]
[AddLeftMono α]
[AddLeftStrictMono α]
:
The sum of two squares is zero iff both elements are zero.
theorem
eq_zero_of_mul_self_add_mul_self_eq_zero
{α : Type u}
[Semiring α]
[LinearOrder α]
{a : α}
{b : α}
[IsRightCancelAdd α]
[NoZeroDivisors α]
[ZeroLEOneClass α]
[ExistsAddOfLE α]
[PosMulMono α]
[AddLeftMono α]
[AddLeftStrictMono α]
(h : a * a + b * b = 0)
:
a = 0
theorem
max_mul_mul_le_max_mul_max
{α : Type u}
[CommSemiring α]
[LinearOrder α]
{a : α}
{d : α}
[PosMulMono α]
[MulPosMono α]
(b : α)
(c : α)
(ha : 0 ≤ a)
(hd : 0 ≤ d)
:
theorem
two_mul_le_add_sq
{α : Type u}
[CommSemiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddLeftReflectLE α]
[AddLeftMono α]
(a : α)
(b : α)
:
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
{α : Type u}
[CommSemiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[MulPosStrictMono α]
[AddLeftReflectLE α]
[AddLeftMono α]
(a : α)
(b : α)
:
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
{α : Type u}
[CommSemiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[MulPosStrictMono α]
[ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
(b : α)
:
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
{α : Type u}
[CommSemiring α]
[LinearOrder α]
[ExistsAddOfLE α]
[MulPosStrictMono α]
[ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
(b : α)
:
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
mul_neg_iff
{α : Type u}
[Ring α]
[LinearOrder α]
{a : α}
{b : α}
[PosMulStrictMono α]
[MulPosStrictMono α]
[AddLeftReflectLT α]
[AddLeftStrictMono α]
:
theorem
mul_nonpos_iff
{α : Type u}
[Ring α]
[LinearOrder α]
{a : α}
{b : α}
[MulPosStrictMono α]
[PosMulStrictMono α]
[AddLeftReflectLE α]
[AddLeftMono α]
:
theorem
mul_nonneg_iff_neg_imp_nonpos
{α : Type u}
[Ring α]
[LinearOrder α]
{a : α}
{b : α}
[PosMulStrictMono α]
[MulPosStrictMono α]
[AddLeftMono α]
[AddLeftReflectLE α]
:
theorem
mul_nonpos_iff_pos_imp_nonpos
{α : Type u}
[Ring α]
[LinearOrder α]
{a : α}
{b : α}
[PosMulStrictMono α]
[MulPosStrictMono α]
[AddLeftMono α]
[AddLeftReflectLE α]
:
theorem
mul_nonpos_iff_neg_imp_nonneg
{α : Type u}
[Ring α]
[LinearOrder α]
{a : α}
{b : α}
[PosMulStrictMono α]
[MulPosStrictMono α]
[AddLeftMono α]
[AddLeftReflectLE α]
:
theorem
neg_one_lt_zero
{α : Type u}
[Ring α]
[LinearOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[AddLeftStrictMono α]
:
-1 < 0
theorem
sub_one_lt
{α : Type u}
[Ring α]
[LinearOrder α]
[ZeroLEOneClass α]
[NeZero 1]
[AddLeftStrictMono α]
(a : α)
:
theorem
mul_self_le_mul_self_of_le_of_neg_le
{α : Type u}
[Ring α]
[LinearOrder α]
{a : α}
{b : α}
[MulPosMono α]
[PosMulMono α]
[AddLeftMono α]
(h₁ : a ≤ b)
(h₂ : -a ≤ b)
: