Ordered rings and semirings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file develops the basics of ordered (semi)rings.
Each typeclass here comprises
- an algebraic class (
semiring,comm_semiring,ring,comm_ring) - an order class (
partial_order,linear_order) - 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 #
ordered_semiring: Semiring with a partial order such that+and*respect≤.strict_ordered_semiring: Nontrivial semiring with a partial order such that+and*respects<.ordered_comm_semiring: Commutative semiring with a partial order such that+and*respect≤.strict_ordered_comm_semiring: Nontrivial commutative semiring with a partial order such that+and*respect<.ordered_ring: Ring with a partial order such that+respects≤and*respects<.ordered_comm_ring: Commutative ring with a partial order such that+respects≤and*respects<.linear_ordered_semiring: Nontrivial semiring with a linear order such that+respects≤and*respects<.linear_ordered_comm_semiring: Nontrivial commutative semiring with a linear order such that+respects≤and*respects<.linear_ordered_ring: Nontrivial ring with a linear order such that+respects≤and*respects<.linear_ordered_comm_ring: Nontrivial commutative ring with a linear order such that+respects≤and*respects<.canonically_ordered_comm_semiring: 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.
ordered_semiringordered_add_comm_monoid& multiplication &*respects≤semiring& partial order structure &+respects≤&*respects≤
strict_ordered_semiringordered_cancel_add_comm_monoid& multiplication &*respects<& nontrivialityordered_semiring&+respects<&*respects<& nontriviality
ordered_comm_semiringordered_semiring& commutativity of multiplicationcomm_semiring& partial order structure &+respects≤&*respects<
strict_ordered_comm_semiringstrict_ordered_semiring& commutativity of multiplicationordered_comm_semiring&+respects<&*respects<& nontriviality
ordered_ringordered_semiring& additive inversesordered_add_comm_group& multiplication &*respects<ring& partial order structure &+respects≤&*respects<
strict_ordered_ringstrict_ordered_semiring& additive inversesordered_semiring&+respects<&*respects<& nontriviality
ordered_comm_ringordered_ring& commutativity of multiplicationordered_comm_semiring& additive inversescomm_ring& partial order structure &+respects≤&*respects<
strict_ordered_comm_ringstrict_ordered_comm_semiring& additive inversesstrict_ordered_ring& commutativity of multiplicationordered_comm_ring&+respects<&*respects<& nontriviality
linear_ordered_semiringstrict_ordered_semiring& totality of the orderlinear_ordered_add_comm_monoid& multiplication & nontriviality &*respects<
linear_ordered_comm_semiringstrict_ordered_comm_semiring& totality of the orderlinear_ordered_semiring& commutativity of multiplication
linear_ordered_ringstrict_ordered_ring& totality of the orderlinear_ordered_semiring& additive inverseslinear_ordered_add_comm_group& multiplication &*respects<domain& linear order structure
linear_ordered_comm_ringstrict_ordered_comm_ring& totality of the orderlinear_ordered_ring& commutativity of multiplicationlinear_ordered_comm_semiring& additive inversesis_domain& linear order structure
Note that order_dual does not satisfy any of the ordered ring typeclasses due to the
zero_le_one field.
theorem
add_one_le_two_mul
{α : Type u}
[has_le α]
[semiring α]
[covariant_class α α has_add.add has_le.le]
{a : α}
(a1 : 1 ≤ a) :
@[instance]
@[class]
- add : α → α → α
- add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), ordered_semiring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), ordered_semiring.nsmul n.succ x = x + ordered_semiring.nsmul n x) . "try_refl_tac"
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
- right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
- zero_mul : ∀ (a : α), 0 * a = 0
- mul_zero : ∀ (a : α), a * 0 = 0
- mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- nat_cast : ℕ → α
- nat_cast_zero : ordered_semiring.nat_cast 0 = 0 . "control_laws_tac"
- nat_cast_succ : (∀ (n : ℕ), ordered_semiring.nat_cast (n + 1) = ordered_semiring.nat_cast n + 1) . "control_laws_tac"
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), ordered_semiring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), ordered_semiring.npow n.succ x = x * ordered_semiring.npow n x) . "try_refl_tac"
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
- zero_le_one : 0 ≤ 1
- mul_le_mul_of_nonneg_left : ∀ (a b c : α), a ≤ b → 0 ≤ c → c * a ≤ c * b
- mul_le_mul_of_nonneg_right : ∀ (a b c : α), a ≤ b → 0 ≤ c → a * c ≤ b * c
An ordered_semiring is a semiring with a partial order such that addition is monotone and
multiplication by a nonnegative number is monotone.
Instances of this typeclass
- ordered_comm_semiring.to_ordered_semiring
- ordered_ring.to_ordered_semiring
- strict_ordered_semiring.to_ordered_semiring
- nat.ordered_semiring
- rat.ordered_semiring
- prod.ordered_semiring
- subsemiring_class.to_ordered_semiring
- subsemiring.to_ordered_semiring
- subalgebra.to_ordered_semiring
- pi.ordered_semiring
- nonneg.ordered_semiring
- real.ordered_semiring
Instances of other typeclasses for ordered_semiring
- ordered_semiring.has_sizeof_inst
@[instance]
@[instance]
@[instance]
@[class]
- add : α → α → α
- add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), ordered_comm_semiring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), ordered_comm_semiring.nsmul n.succ x = x + ordered_comm_semiring.nsmul n x) . "try_refl_tac"
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
- right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
- zero_mul : ∀ (a : α), 0 * a = 0
- mul_zero : ∀ (a : α), a * 0 = 0
- mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- nat_cast : ℕ → α
- nat_cast_zero : ordered_comm_semiring.nat_cast 0 = 0 . "control_laws_tac"
- nat_cast_succ : (∀ (n : ℕ), ordered_comm_semiring.nat_cast (n + 1) = ordered_comm_semiring.nat_cast n + 1) . "control_laws_tac"
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), ordered_comm_semiring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), ordered_comm_semiring.npow n.succ x = x * ordered_comm_semiring.npow n x) . "try_refl_tac"
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
- zero_le_one : 0 ≤ 1
- mul_le_mul_of_nonneg_left : ∀ (a b c : α), a ≤ b → 0 ≤ c → c * a ≤ c * b
- mul_le_mul_of_nonneg_right : ∀ (a b c : α), a ≤ b → 0 ≤ c → a * c ≤ b * c
- mul_comm : ∀ (a b : α), a * b = b * a
An ordered_comm_semiring is a commutative semiring with a partial order such that addition is
monotone and multiplication by a nonnegative number is monotone.
Instances of this typeclass
- ordered_comm_ring.to_ordered_comm_semiring
- strict_ordered_comm_semiring.to_ordered_comm_semiring
- canonically_ordered_comm_semiring.to_ordered_comm_semiring
- nat.ordered_comm_semiring
- with_bot.ordered_comm_semiring
- prod.ordered_comm_semiring
- subsemiring_class.to_ordered_comm_semiring
- subsemiring.to_ordered_comm_semiring
- subalgebra.to_ordered_comm_semiring
- pi.ordered_comm_semiring
- nonneg.ordered_comm_semiring
- nnreal.ordered_comm_semiring
Instances of other typeclasses for ordered_comm_semiring
- ordered_comm_semiring.has_sizeof_inst
@[instance]
@[class]
- add : α → α → α
- add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), ordered_ring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), ordered_ring.nsmul n.succ x = x + ordered_ring.nsmul n x) . "try_refl_tac"
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
- zsmul : ℤ → α → α
- zsmul_zero' : (∀ (a : α), ordered_ring.zsmul 0 a = 0) . "try_refl_tac"
- zsmul_succ' : (∀ (n : ℕ) (a : α), ordered_ring.zsmul (int.of_nat n.succ) a = a + ordered_ring.zsmul (int.of_nat n) a) . "try_refl_tac"
- zsmul_neg' : (∀ (n : ℕ) (a : α), ordered_ring.zsmul -[1+ n] a = -ordered_ring.zsmul ↑(n.succ) a) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- int_cast : ℤ → α
- nat_cast : ℕ → α
- one : α
- nat_cast_zero : ordered_ring.nat_cast 0 = 0 . "control_laws_tac"
- nat_cast_succ : (∀ (n : ℕ), ordered_ring.nat_cast (n + 1) = ordered_ring.nat_cast n + 1) . "control_laws_tac"
- int_cast_of_nat : (∀ (n : ℕ), ordered_ring.int_cast ↑n = ↑n) . "control_laws_tac"
- int_cast_neg_succ_of_nat : (∀ (n : ℕ), ordered_ring.int_cast (-↑(n + 1)) = -↑(n + 1)) . "control_laws_tac"
- mul : α → α → α
- mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), ordered_ring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), ordered_ring.npow n.succ x = x * ordered_ring.npow n x) . "try_refl_tac"
- left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
- right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
- zero_le_one : 0 ≤ 1
- mul_nonneg : ∀ (a b : α), 0 ≤ a → 0 ≤ b → 0 ≤ a * b
An ordered_ring is a ring with a partial order such that addition is monotone and
multiplication by a nonnegative number is monotone.
Instances of this typeclass
Instances of other typeclasses for ordered_ring
- ordered_ring.has_sizeof_inst
@[instance]
@[instance]
@[class]
- add : α → α → α
- add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), ordered_comm_ring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), ordered_comm_ring.nsmul n.succ x = x + ordered_comm_ring.nsmul n x) . "try_refl_tac"
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
- zsmul : ℤ → α → α
- zsmul_zero' : (∀ (a : α), ordered_comm_ring.zsmul 0 a = 0) . "try_refl_tac"
- zsmul_succ' : (∀ (n : ℕ) (a : α), ordered_comm_ring.zsmul (int.of_nat n.succ) a = a + ordered_comm_ring.zsmul (int.of_nat n) a) . "try_refl_tac"
- zsmul_neg' : (∀ (n : ℕ) (a : α), ordered_comm_ring.zsmul -[1+ n] a = -ordered_comm_ring.zsmul ↑(n.succ) a) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- int_cast : ℤ → α
- nat_cast : ℕ → α
- one : α
- nat_cast_zero : ordered_comm_ring.nat_cast 0 = 0 . "control_laws_tac"
- nat_cast_succ : (∀ (n : ℕ), ordered_comm_ring.nat_cast (n + 1) = ordered_comm_ring.nat_cast n + 1) . "control_laws_tac"
- int_cast_of_nat : (∀ (n : ℕ), ordered_comm_ring.int_cast ↑n = ↑n) . "control_laws_tac"
- int_cast_neg_succ_of_nat : (∀ (n : ℕ), ordered_comm_ring.int_cast (-↑(n + 1)) = -↑(n + 1)) . "control_laws_tac"
- mul : α → α → α
- mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), ordered_comm_ring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), ordered_comm_ring.npow n.succ x = x * ordered_comm_ring.npow n x) . "try_refl_tac"
- left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
- right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
- zero_le_one : 0 ≤ 1
- mul_nonneg : ∀ (a b : α), 0 ≤ a → 0 ≤ b → 0 ≤ a * b
- mul_comm : ∀ (a b : α), a * b = b * a
An ordered_comm_ring is a commutative ring with a partial order such that addition is monotone
and multiplication by a nonnegative number is monotone.
Instances of this typeclass
Instances of other typeclasses for ordered_comm_ring
- ordered_comm_ring.has_sizeof_inst
@[instance]
@[instance]
def
strict_ordered_semiring.to_ordered_cancel_add_comm_monoid
(α : Type u)
[self : strict_ordered_semiring α] :
@[class]
- add : α → α → α
- add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), strict_ordered_semiring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), strict_ordered_semiring.nsmul n.succ x = x + strict_ordered_semiring.nsmul n x) . "try_refl_tac"
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
- right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
- zero_mul : ∀ (a : α), 0 * a = 0
- mul_zero : ∀ (a : α), a * 0 = 0
- mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- nat_cast : ℕ → α
- nat_cast_zero : strict_ordered_semiring.nat_cast 0 = 0 . "control_laws_tac"
- nat_cast_succ : (∀ (n : ℕ), strict_ordered_semiring.nat_cast (n + 1) = strict_ordered_semiring.nat_cast n + 1) . "control_laws_tac"
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), strict_ordered_semiring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), strict_ordered_semiring.npow n.succ x = x * strict_ordered_semiring.npow n x) . "try_refl_tac"
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
- le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
- exists_pair_ne : ∃ (x y : α), x ≠ y
- zero_le_one : 0 ≤ 1
- mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b → 0 < c → c * a < c * b
- mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b → 0 < c → a * c < b * c
A strict_ordered_semiring is a nontrivial semiring with a partial order such that addition is
strictly monotone and multiplication by a positive number is strictly monotone.
Instances of this typeclass
- strict_ordered_comm_semiring.to_strict_ordered_semiring
- linear_ordered_semiring.to_strict_ordered_semiring
- strict_ordered_ring.to_strict_ordered_semiring
- nat.strict_ordered_semiring
- subsemiring_class.to_strict_ordered_semiring
- subsemiring.to_strict_ordered_semiring
- subalgebra.to_strict_ordered_semiring
- nonneg.strict_ordered_semiring
- real.strict_ordered_semiring
- nnreal.strict_ordered_semiring
Instances of other typeclasses for strict_ordered_semiring
- strict_ordered_semiring.has_sizeof_inst
@[instance]
def
strict_ordered_semiring.to_semiring
(α : Type u)
[self : strict_ordered_semiring α] :
semiring α
@[instance]
def
strict_ordered_comm_semiring.to_strict_ordered_semiring
(α : Type u)
[self : strict_ordered_comm_semiring α] :
@[class]
- add : α → α → α
- add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), strict_ordered_comm_semiring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), strict_ordered_comm_semiring.nsmul n.succ x = x + strict_ordered_comm_semiring.nsmul n x) . "try_refl_tac"
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
- right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
- zero_mul : ∀ (a : α), 0 * a = 0
- mul_zero : ∀ (a : α), a * 0 = 0
- mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- nat_cast : ℕ → α
- nat_cast_zero : strict_ordered_comm_semiring.nat_cast 0 = 0 . "control_laws_tac"
- nat_cast_succ : (∀ (n : ℕ), strict_ordered_comm_semiring.nat_cast (n + 1) = strict_ordered_comm_semiring.nat_cast n + 1) . "control_laws_tac"
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), strict_ordered_comm_semiring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), strict_ordered_comm_semiring.npow n.succ x = x * strict_ordered_comm_semiring.npow n x) . "try_refl_tac"
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
- le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
- exists_pair_ne : ∃ (x y : α), x ≠ y
- zero_le_one : 0 ≤ 1
- mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b → 0 < c → c * a < c * b
- mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b → 0 < c → a * c < b * c
- mul_comm : ∀ (a b : α), a * b = b * a
A strict_ordered_comm_semiring is a commutative semiring with a partial order such that
addition is strictly monotone and multiplication by a positive number is strictly monotone.
Instances of this typeclass
- linear_ordered_comm_semiring.to_strict_ordered_comm_semiring
- strict_ordered_comm_ring.to_strict_ordered_comm_semiring
- nat.strict_ordered_comm_semiring
- subsemiring_class.to_strict_ordered_comm_semiring
- subsemiring.to_strict_ordered_comm_semiring
- subalgebra.to_strict_ordered_comm_semiring
- nonneg.strict_ordered_comm_semiring
- real.strict_ordered_comm_semiring
Instances of other typeclasses for strict_ordered_comm_semiring
- strict_ordered_comm_semiring.has_sizeof_inst
@[instance]
def
strict_ordered_comm_semiring.to_comm_semiring
(α : Type u)
[self : strict_ordered_comm_semiring α] :
@[class]
- add : α → α → α
- add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), strict_ordered_ring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), strict_ordered_ring.nsmul n.succ x = x + strict_ordered_ring.nsmul n x) . "try_refl_tac"
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
- zsmul : ℤ → α → α
- zsmul_zero' : (∀ (a : α), strict_ordered_ring.zsmul 0 a = 0) . "try_refl_tac"
- zsmul_succ' : (∀ (n : ℕ) (a : α), strict_ordered_ring.zsmul (int.of_nat n.succ) a = a + strict_ordered_ring.zsmul (int.of_nat n) a) . "try_refl_tac"
- zsmul_neg' : (∀ (n : ℕ) (a : α), strict_ordered_ring.zsmul -[1+ n] a = -strict_ordered_ring.zsmul ↑(n.succ) a) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- int_cast : ℤ → α
- nat_cast : ℕ → α
- one : α
- nat_cast_zero : strict_ordered_ring.nat_cast 0 = 0 . "control_laws_tac"
- nat_cast_succ : (∀ (n : ℕ), strict_ordered_ring.nat_cast (n + 1) = strict_ordered_ring.nat_cast n + 1) . "control_laws_tac"
- int_cast_of_nat : (∀ (n : ℕ), strict_ordered_ring.int_cast ↑n = ↑n) . "control_laws_tac"
- int_cast_neg_succ_of_nat : (∀ (n : ℕ), strict_ordered_ring.int_cast (-↑(n + 1)) = -↑(n + 1)) . "control_laws_tac"
- mul : α → α → α
- mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), strict_ordered_ring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), strict_ordered_ring.npow n.succ x = x * strict_ordered_ring.npow n x) . "try_refl_tac"
- left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
- right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
- exists_pair_ne : ∃ (x y : α), x ≠ y
- zero_le_one : 0 ≤ 1
- mul_pos : ∀ (a b : α), 0 < a → 0 < b → 0 < a * b
A strict_ordered_ring is a ring with a partial order such that addition is strictly monotone
and multiplication by a positive number is strictly monotone.
Instances of this typeclass
Instances of other typeclasses for strict_ordered_ring
- strict_ordered_ring.has_sizeof_inst
@[instance]
@[instance]
@[instance]
@[instance]
@[class]
- add : α → α → α
- add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), strict_ordered_comm_ring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), strict_ordered_comm_ring.nsmul n.succ x = x + strict_ordered_comm_ring.nsmul n x) . "try_refl_tac"
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
- zsmul : ℤ → α → α
- zsmul_zero' : (∀ (a : α), strict_ordered_comm_ring.zsmul 0 a = 0) . "try_refl_tac"
- zsmul_succ' : (∀ (n : ℕ) (a : α), strict_ordered_comm_ring.zsmul (int.of_nat n.succ) a = a + strict_ordered_comm_ring.zsmul (int.of_nat n) a) . "try_refl_tac"
- zsmul_neg' : (∀ (n : ℕ) (a : α), strict_ordered_comm_ring.zsmul -[1+ n] a = -strict_ordered_comm_ring.zsmul ↑(n.succ) a) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- int_cast : ℤ → α
- nat_cast : ℕ → α
- one : α
- nat_cast_zero : strict_ordered_comm_ring.nat_cast 0 = 0 . "control_laws_tac"
- nat_cast_succ : (∀ (n : ℕ), strict_ordered_comm_ring.nat_cast (n + 1) = strict_ordered_comm_ring.nat_cast n + 1) . "control_laws_tac"
- int_cast_of_nat : (∀ (n : ℕ), strict_ordered_comm_ring.int_cast ↑n = ↑n) . "control_laws_tac"
- int_cast_neg_succ_of_nat : (∀ (n : ℕ), strict_ordered_comm_ring.int_cast (-↑(n + 1)) = -↑(n + 1)) . "control_laws_tac"
- mul : α → α → α
- mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), strict_ordered_comm_ring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), strict_ordered_comm_ring.npow n.succ x = x * strict_ordered_comm_ring.npow n x) . "try_refl_tac"
- left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
- right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
- exists_pair_ne : ∃ (x y : α), x ≠ y
- zero_le_one : 0 ≤ 1
- mul_pos : ∀ (a b : α), 0 < a → 0 < b → 0 < a * b
- mul_comm : ∀ (a b : α), a * b = b * a
A strict_ordered_comm_ring is a commutative ring with a partial order such that addition is
strictly monotone and multiplication by a positive number is strictly monotone.
Instances of this typeclass
Instances of other typeclasses for strict_ordered_comm_ring
- strict_ordered_comm_ring.has_sizeof_inst
@[instance]
def
strict_ordered_comm_ring.to_strict_ordered_ring
(α : Type u_2)
[self : strict_ordered_comm_ring α] :
@[class]
- add : α → α → α
- add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), linear_ordered_semiring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), linear_ordered_semiring.nsmul n.succ x = x + linear_ordered_semiring.nsmul n x) . "try_refl_tac"
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
- right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
- zero_mul : ∀ (a : α), 0 * a = 0
- mul_zero : ∀ (a : α), a * 0 = 0
- mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- nat_cast : ℕ → α
- nat_cast_zero : linear_ordered_semiring.nat_cast 0 = 0 . "control_laws_tac"
- nat_cast_succ : (∀ (n : ℕ), linear_ordered_semiring.nat_cast (n + 1) = linear_ordered_semiring.nat_cast n + 1) . "control_laws_tac"
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), linear_ordered_semiring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), linear_ordered_semiring.npow n.succ x = x * linear_ordered_semiring.npow n x) . "try_refl_tac"
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
- le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
- exists_pair_ne : ∃ (x y : α), x ≠ y
- zero_le_one : 0 ≤ 1
- mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b → 0 < c → c * a < c * b
- mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b → 0 < c → a * c < b * c
- le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
- decidable_le : decidable_rel has_le.le
- decidable_eq : decidable_eq α
- decidable_lt : decidable_rel has_lt.lt
- max : α → α → α
- max_def : linear_ordered_semiring.max = max_default . "reflexivity"
- min : α → α → α
- min_def : linear_ordered_semiring.min = min_default . "reflexivity"
A linear_ordered_semiring is a nontrivial semiring with a linear order such that
addition is monotone and multiplication by a positive number is strictly monotone.
Instances of this typeclass
- linear_ordered_comm_semiring.to_linear_ordered_semiring
- linear_ordered_ring.to_linear_ordered_semiring
- nat.linear_ordered_semiring
- rat.linear_ordered_semiring
- subsemiring_class.to_linear_ordered_semiring
- subsemiring.to_linear_ordered_semiring
- subalgebra.to_linear_ordered_semiring
- nonneg.linear_ordered_semiring
- real.linear_ordered_semiring
- nnreal.linear_ordered_semiring
Instances of other typeclasses for linear_ordered_semiring
- linear_ordered_semiring.has_sizeof_inst
@[instance]
def
linear_ordered_semiring.to_linear_ordered_add_comm_monoid
(α : Type u)
[self : linear_ordered_semiring α] :
@[instance]
def
linear_ordered_semiring.to_strict_ordered_semiring
(α : Type u)
[self : linear_ordered_semiring α] :
@[instance]
def
linear_ordered_comm_semiring.to_linear_ordered_semiring
(α : Type u_2)
[self : linear_ordered_comm_semiring α] :
@[class]
- add : α → α → α
- add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), linear_ordered_comm_semiring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), linear_ordered_comm_semiring.nsmul n.succ x = x + linear_ordered_comm_semiring.nsmul n x) . "try_refl_tac"
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
- right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
- zero_mul : ∀ (a : α), 0 * a = 0
- mul_zero : ∀ (a : α), a * 0 = 0
- mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- nat_cast : ℕ → α
- nat_cast_zero : linear_ordered_comm_semiring.nat_cast 0 = 0 . "control_laws_tac"
- nat_cast_succ : (∀ (n : ℕ), linear_ordered_comm_semiring.nat_cast (n + 1) = linear_ordered_comm_semiring.nat_cast n + 1) . "control_laws_tac"
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), linear_ordered_comm_semiring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), linear_ordered_comm_semiring.npow n.succ x = x * linear_ordered_comm_semiring.npow n x) . "try_refl_tac"
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
- le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
- exists_pair_ne : ∃ (x y : α), x ≠ y
- zero_le_one : 0 ≤ 1
- mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b → 0 < c → c * a < c * b
- mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b → 0 < c → a * c < b * c
- mul_comm : ∀ (a b : α), a * b = b * a
- le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
- decidable_le : decidable_rel has_le.le
- decidable_eq : decidable_eq α
- decidable_lt : decidable_rel has_lt.lt
- max : α → α → α
- max_def : linear_ordered_comm_semiring.max = max_default . "reflexivity"
- min : α → α → α
- min_def : linear_ordered_comm_semiring.min = min_default . "reflexivity"
A linear_ordered_comm_semiring is a nontrivial commutative semiring with a linear order such
that addition is monotone and multiplication by a positive number is strictly monotone.
Instances of this typeclass
Instances of other typeclasses for linear_ordered_comm_semiring
- linear_ordered_comm_semiring.has_sizeof_inst
@[instance]
def
linear_ordered_comm_semiring.to_strict_ordered_comm_semiring
(α : Type u_2)
[self : linear_ordered_comm_semiring α] :
@[instance]
@[class]
- add : α → α → α
- add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), linear_ordered_ring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), linear_ordered_ring.nsmul n.succ x = x + linear_ordered_ring.nsmul n x) . "try_refl_tac"
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
- zsmul : ℤ → α → α
- zsmul_zero' : (∀ (a : α), linear_ordered_ring.zsmul 0 a = 0) . "try_refl_tac"
- zsmul_succ' : (∀ (n : ℕ) (a : α), linear_ordered_ring.zsmul (int.of_nat n.succ) a = a + linear_ordered_ring.zsmul (int.of_nat n) a) . "try_refl_tac"
- zsmul_neg' : (∀ (n : ℕ) (a : α), linear_ordered_ring.zsmul -[1+ n] a = -linear_ordered_ring.zsmul ↑(n.succ) a) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- int_cast : ℤ → α
- nat_cast : ℕ → α
- one : α
- nat_cast_zero : linear_ordered_ring.nat_cast 0 = 0 . "control_laws_tac"
- nat_cast_succ : (∀ (n : ℕ), linear_ordered_ring.nat_cast (n + 1) = linear_ordered_ring.nat_cast n + 1) . "control_laws_tac"
- int_cast_of_nat : (∀ (n : ℕ), linear_ordered_ring.int_cast ↑n = ↑n) . "control_laws_tac"
- int_cast_neg_succ_of_nat : (∀ (n : ℕ), linear_ordered_ring.int_cast (-↑(n + 1)) = -↑(n + 1)) . "control_laws_tac"
- mul : α → α → α
- mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), linear_ordered_ring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), linear_ordered_ring.npow n.succ x = x * linear_ordered_ring.npow n x) . "try_refl_tac"
- left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
- right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
- exists_pair_ne : ∃ (x y : α), x ≠ y
- zero_le_one : 0 ≤ 1
- mul_pos : ∀ (a b : α), 0 < a → 0 < b → 0 < a * b
- le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
- decidable_le : decidable_rel has_le.le
- decidable_eq : decidable_eq α
- decidable_lt : decidable_rel has_lt.lt
- max : α → α → α
- max_def : linear_ordered_ring.max = max_default . "reflexivity"
- min : α → α → α
- min_def : linear_ordered_ring.min = min_default . "reflexivity"
A linear_ordered_ring is a ring with a linear order such that addition is monotone and
multiplication by a positive number is strictly monotone.
Instances of this typeclass
Instances of other typeclasses for linear_ordered_ring
- linear_ordered_ring.has_sizeof_inst
@[instance]
@[class]
- add : α → α → α
- add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), linear_ordered_comm_ring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), linear_ordered_comm_ring.nsmul n.succ x = x + linear_ordered_comm_ring.nsmul n x) . "try_refl_tac"
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
- zsmul : ℤ → α → α
- zsmul_zero' : (∀ (a : α), linear_ordered_comm_ring.zsmul 0 a = 0) . "try_refl_tac"
- zsmul_succ' : (∀ (n : ℕ) (a : α), linear_ordered_comm_ring.zsmul (int.of_nat n.succ) a = a + linear_ordered_comm_ring.zsmul (int.of_nat n) a) . "try_refl_tac"
- zsmul_neg' : (∀ (n : ℕ) (a : α), linear_ordered_comm_ring.zsmul -[1+ n] a = -linear_ordered_comm_ring.zsmul ↑(n.succ) a) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- int_cast : ℤ → α
- nat_cast : ℕ → α
- one : α
- nat_cast_zero : linear_ordered_comm_ring.nat_cast 0 = 0 . "control_laws_tac"
- nat_cast_succ : (∀ (n : ℕ), linear_ordered_comm_ring.nat_cast (n + 1) = linear_ordered_comm_ring.nat_cast n + 1) . "control_laws_tac"
- int_cast_of_nat : (∀ (n : ℕ), linear_ordered_comm_ring.int_cast ↑n = ↑n) . "control_laws_tac"
- int_cast_neg_succ_of_nat : (∀ (n : ℕ), linear_ordered_comm_ring.int_cast (-↑(n + 1)) = -↑(n + 1)) . "control_laws_tac"
- mul : α → α → α
- mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), linear_ordered_comm_ring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), linear_ordered_comm_ring.npow n.succ x = x * linear_ordered_comm_ring.npow n x) . "try_refl_tac"
- left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
- right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
- exists_pair_ne : ∃ (x y : α), x ≠ y
- zero_le_one : 0 ≤ 1
- mul_pos : ∀ (a b : α), 0 < a → 0 < b → 0 < a * b
- le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
- decidable_le : decidable_rel has_le.le
- decidable_eq : decidable_eq α
- decidable_lt : decidable_rel has_lt.lt
- max : α → α → α
- max_def : linear_ordered_comm_ring.max = max_default . "reflexivity"
- min : α → α → α
- min_def : linear_ordered_comm_ring.min = min_default . "reflexivity"
- mul_comm : ∀ (a b : α), a * b = b * a
A linear_ordered_comm_ring is a commutative ring with a linear order such that addition is
monotone and multiplication by a positive number is strictly monotone.
Instances of this typeclass
Instances of other typeclasses for linear_ordered_comm_ring
- linear_ordered_comm_ring.has_sizeof_inst
@[instance]
def
linear_ordered_comm_ring.to_linear_ordered_ring
(α : Type u)
[self : linear_ordered_comm_ring α] :
@[instance]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[simp]
theorem
one_le_mul_of_one_le_of_one_le
{α : Type u}
[ordered_semiring α]
{a b : α}
(ha : 1 ≤ a)
(hb : 1 ≤ b) :
theorem
mul_le_one
{α : Type u}
[ordered_semiring α]
{a b : α}
(ha : a ≤ 1)
(hb' : 0 ≤ b)
(hb : b ≤ 1) :
theorem
one_lt_mul_of_le_of_lt
{α : Type u}
[ordered_semiring α]
{a b : α}
(ha : 1 ≤ a)
(hb : 1 < b) :
theorem
one_lt_mul_of_lt_of_le
{α : Type u}
[ordered_semiring α]
{a b : α}
(ha : 1 < a)
(hb : 1 ≤ b) :
Alias of one_lt_mul_of_le_of_lt.
theorem
mul_lt_one_of_nonneg_of_lt_one_left
{α : Type u}
[ordered_semiring α]
{a b : α}
(ha₀ : 0 ≤ a)
(ha : a < 1)
(hb : b ≤ 1) :
theorem
mul_lt_one_of_nonneg_of_lt_one_right
{α : Type u}
[ordered_semiring α]
{a b : α}
(ha : a ≤ 1)
(hb₀ : 0 ≤ b)
(hb : b < 1) :
@[protected, instance]
Equations
- ordered_ring.to_ordered_semiring = {add := ordered_ring.add _inst_1, add_assoc := _, zero := ordered_ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := ordered_ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := ordered_ring.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := ordered_ring.one _inst_1, one_mul := _, mul_one := _, nat_cast := ordered_ring.nat_cast _inst_1, nat_cast_zero := _, nat_cast_succ := _, npow := ordered_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, le := ordered_ring.le _inst_1, lt := ordered_ring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_le_mul_of_nonneg_left := _, mul_le_mul_of_nonneg_right := _}
theorem
mul_le_mul_of_nonpos_left
{α : Type u}
[ordered_ring α]
{a b c : α}
(h : b ≤ a)
(hc : c ≤ 0) :
theorem
mul_le_mul_of_nonpos_right
{α : Type u}
[ordered_ring α]
{a b c : α}
(h : b ≤ a)
(hc : c ≤ 0) :
theorem
mul_nonneg_of_nonpos_of_nonpos
{α : Type u}
[ordered_ring α]
{a b : α}
(ha : a ≤ 0)
(hb : b ≤ 0) :
Variant of mul_le_of_le_one_left for b non-positive instead of non-negative.
Variant of le_mul_of_one_le_left for b non-positive instead of non-negative.
Variant of mul_le_of_le_one_right for a non-positive instead of non-negative.
Variant of le_mul_of_one_le_right for a non-positive instead of non-negative.
theorem
antitone_mul_left
{α : Type u}
[ordered_ring α]
{a : α}
(ha : a ≤ 0) :
antitone (has_mul.mul a)
@[protected, instance]
Equations
- ordered_comm_ring.to_ordered_comm_semiring = {add := ordered_semiring.add ordered_ring.to_ordered_semiring, add_assoc := _, zero := ordered_semiring.zero ordered_ring.to_ordered_semiring, zero_add := _, add_zero := _, nsmul := ordered_semiring.nsmul ordered_ring.to_ordered_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := ordered_semiring.mul ordered_ring.to_ordered_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := ordered_semiring.one ordered_ring.to_ordered_semiring, one_mul := _, mul_one := _, nat_cast := ordered_semiring.nat_cast ordered_ring.to_ordered_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := ordered_semiring.npow ordered_ring.to_ordered_semiring, npow_zero' := _, npow_succ' := _, le := ordered_semiring.le ordered_ring.to_ordered_semiring, lt := ordered_semiring.lt ordered_ring.to_ordered_semiring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_le_mul_of_nonneg_left := _, mul_le_mul_of_nonneg_right := _, mul_comm := _}
@[protected, instance]
@[protected, instance]
@[reducible]
def
strict_ordered_semiring.to_ordered_semiring'
{α : Type u}
[strict_ordered_semiring α]
[decidable_rel has_le.le] :
A choice-free version of strict_ordered_semiring.to_ordered_semiring to avoid using choice in
basic nat lemmas.
Equations
- strict_ordered_semiring.to_ordered_semiring' = {add := strict_ordered_semiring.add _inst_1, add_assoc := _, zero := strict_ordered_semiring.zero _inst_1, zero_add := _, add_zero := _, nsmul := strict_ordered_semiring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := strict_ordered_semiring.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := strict_ordered_semiring.one _inst_1, one_mul := _, mul_one := _, nat_cast := strict_ordered_semiring.nat_cast _inst_1, nat_cast_zero := _, nat_cast_succ := _, npow := strict_ordered_semiring.npow _inst_1, npow_zero' := _, npow_succ' := _, le := strict_ordered_semiring.le _inst_1, lt := strict_ordered_semiring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_le_mul_of_nonneg_left := _, mul_le_mul_of_nonneg_right := _}
@[protected, instance]
Equations
- strict_ordered_semiring.to_ordered_semiring = {add := strict_ordered_semiring.add _inst_1, add_assoc := _, zero := strict_ordered_semiring.zero _inst_1, zero_add := _, add_zero := _, nsmul := strict_ordered_semiring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := strict_ordered_semiring.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := strict_ordered_semiring.one _inst_1, one_mul := _, mul_one := _, nat_cast := strict_ordered_semiring.nat_cast _inst_1, nat_cast_zero := _, nat_cast_succ := _, npow := strict_ordered_semiring.npow _inst_1, npow_zero' := _, npow_succ' := _, le := strict_ordered_semiring.le _inst_1, lt := strict_ordered_semiring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_le_mul_of_nonneg_left := _, mul_le_mul_of_nonneg_right := _}
theorem
mul_self_lt_mul_self
{α : Type u}
[strict_ordered_semiring α]
{a b : α}
(h1 : 0 ≤ a)
(h2 : a < b) :
theorem
strict_mono_on_mul_self
{α : Type u}
[strict_ordered_semiring α] :
strict_mono_on (λ (x : α), x * x) {x : α | 0 ≤ x}
@[protected]
theorem
decidable.mul_lt_mul''
{α : Type u}
[strict_ordered_semiring α]
{a b c d : α}
[decidable_rel has_le.le]
(h1 : a < c)
(h2 : b < d)
(h3 : 0 ≤ a)
(h4 : 0 ≤ b) :
theorem
strict_mono_mul_left_of_pos
{α : Type u}
[strict_ordered_semiring α]
{a : α}
(ha : 0 < a) :
strict_mono (λ (x : α), a * x)
theorem
strict_mono_mul_right_of_pos
{α : Type u}
[strict_ordered_semiring α]
{a : α}
(ha : 0 < a) :
strict_mono (λ (x : α), x * a)
theorem
strict_mono.mul_const
{α : Type u}
{β : Type u_1}
[strict_ordered_semiring α]
{a : α}
[preorder β]
{f : β → α}
(hf : strict_mono f)
(ha : 0 < a) :
strict_mono (λ (x : β), f x * a)
theorem
strict_mono.const_mul
{α : Type u}
{β : Type u_1}
[strict_ordered_semiring α]
{a : α}
[preorder β]
{f : β → α}
(hf : strict_mono f)
(ha : 0 < a) :
strict_mono (λ (x : β), a * f x)
theorem
strict_anti.mul_const
{α : Type u}
{β : Type u_1}
[strict_ordered_semiring α]
{a : α}
[preorder β]
{f : β → α}
(hf : strict_anti f)
(ha : 0 < a) :
strict_anti (λ (x : β), f x * a)
theorem
strict_anti.const_mul
{α : Type u}
{β : Type u_1}
[strict_ordered_semiring α]
{a : α}
[preorder β]
{f : β → α}
(hf : strict_anti f)
(ha : 0 < a) :
strict_anti (λ (x : β), a * f x)
theorem
strict_mono.mul_monotone
{α : Type u}
{β : Type u_1}
[strict_ordered_semiring α]
[preorder β]
{f g : β → α}
(hf : strict_mono f)
(hg : monotone g)
(hf₀ : ∀ (x : β), 0 ≤ f x)
(hg₀ : ∀ (x : β), 0 < g x) :
strict_mono (f * g)
theorem
monotone.mul_strict_mono
{α : Type u}
{β : Type u_1}
[strict_ordered_semiring α]
[preorder β]
{f g : β → α}
(hf : monotone f)
(hg : strict_mono g)
(hf₀ : ∀ (x : β), 0 < f x)
(hg₀ : ∀ (x : β), 0 ≤ g x) :
strict_mono (f * g)
theorem
strict_mono.mul
{α : Type u}
{β : Type u_1}
[strict_ordered_semiring α]
[preorder β]
{f g : β → α}
(hf : strict_mono f)
(hg : strict_mono g)
(hf₀ : ∀ (x : β), 0 ≤ f x)
(hg₀ : ∀ (x : β), 0 ≤ g x) :
strict_mono (f * g)
@[protected, instance]
@[reducible]
def
strict_ordered_comm_semiring.to_ordered_comm_semiring'
{α : Type u}
[strict_ordered_comm_semiring α]
[decidable_rel has_le.le] :
A choice-free version of strict_ordered_comm_semiring.to_ordered_comm_semiring to avoid using
choice in basic nat lemmas.
Equations
- strict_ordered_comm_semiring.to_ordered_comm_semiring' = {add := strict_ordered_comm_semiring.add _inst_1, add_assoc := _, zero := strict_ordered_comm_semiring.zero _inst_1, zero_add := _, add_zero := _, nsmul := strict_ordered_comm_semiring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := strict_ordered_comm_semiring.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := strict_ordered_comm_semiring.one _inst_1, one_mul := _, mul_one := _, nat_cast := strict_ordered_comm_semiring.nat_cast _inst_1, nat_cast_zero := _, nat_cast_succ := _, npow := strict_ordered_comm_semiring.npow _inst_1, npow_zero' := _, npow_succ' := _, le := strict_ordered_comm_semiring.le _inst_1, lt := strict_ordered_comm_semiring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_le_mul_of_nonneg_left := _, mul_le_mul_of_nonneg_right := _, mul_comm := _}
@[protected, instance]
def
strict_ordered_comm_semiring.to_ordered_comm_semiring
{α : Type u}
[strict_ordered_comm_semiring α] :
Equations
- strict_ordered_comm_semiring.to_ordered_comm_semiring = {add := strict_ordered_comm_semiring.add _inst_1, add_assoc := _, zero := strict_ordered_comm_semiring.zero _inst_1, zero_add := _, add_zero := _, nsmul := strict_ordered_comm_semiring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := strict_ordered_comm_semiring.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := strict_ordered_comm_semiring.one _inst_1, one_mul := _, mul_one := _, nat_cast := strict_ordered_comm_semiring.nat_cast _inst_1, nat_cast_zero := _, nat_cast_succ := _, npow := strict_ordered_comm_semiring.npow _inst_1, npow_zero' := _, npow_succ' := _, le := strict_ordered_comm_semiring.le _inst_1, lt := strict_ordered_comm_semiring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_le_mul_of_nonneg_left := _, mul_le_mul_of_nonneg_right := _, mul_comm := _}
@[protected, instance]
Equations
- strict_ordered_ring.to_strict_ordered_semiring = {add := strict_ordered_ring.add _inst_1, add_assoc := _, zero := strict_ordered_ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := strict_ordered_ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := strict_ordered_ring.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := strict_ordered_ring.one _inst_1, one_mul := _, mul_one := _, nat_cast := strict_ordered_ring.nat_cast _inst_1, nat_cast_zero := _, nat_cast_succ := _, npow := strict_ordered_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, le := strict_ordered_ring.le _inst_1, lt := strict_ordered_ring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _}
@[reducible]
def
strict_ordered_ring.to_ordered_ring'
{α : Type u}
[strict_ordered_ring α]
[decidable_rel has_le.le] :
A choice-free version of strict_ordered_ring.to_ordered_ring to avoid using choice in basic
int lemmas.
Equations
- strict_ordered_ring.to_ordered_ring' = {add := strict_ordered_ring.add _inst_1, add_assoc := _, zero := strict_ordered_ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := strict_ordered_ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := strict_ordered_ring.neg _inst_1, sub := strict_ordered_ring.sub _inst_1, sub_eq_add_neg := _, zsmul := strict_ordered_ring.zsmul _inst_1, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := strict_ordered_ring.int_cast _inst_1, nat_cast := strict_ordered_ring.nat_cast _inst_1, one := strict_ordered_ring.one _inst_1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := strict_ordered_ring.mul _inst_1, mul_assoc := _, one_mul := _, mul_one := _, npow := strict_ordered_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := strict_ordered_ring.le _inst_1, lt := strict_ordered_ring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_nonneg := _}
@[protected, instance]
Equations
- strict_ordered_ring.to_ordered_ring = {add := strict_ordered_ring.add _inst_1, add_assoc := _, zero := strict_ordered_ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := strict_ordered_ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := strict_ordered_ring.neg _inst_1, sub := strict_ordered_ring.sub _inst_1, sub_eq_add_neg := _, zsmul := strict_ordered_ring.zsmul _inst_1, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := strict_ordered_ring.int_cast _inst_1, nat_cast := strict_ordered_ring.nat_cast _inst_1, one := strict_ordered_ring.one _inst_1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := strict_ordered_ring.mul _inst_1, mul_assoc := _, one_mul := _, mul_one := _, npow := strict_ordered_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := strict_ordered_ring.le _inst_1, lt := strict_ordered_ring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_nonneg := _}
theorem
mul_lt_mul_of_neg_left
{α : Type u}
[strict_ordered_ring α]
{a b c : α}
(h : b < a)
(hc : c < 0) :
theorem
mul_lt_mul_of_neg_right
{α : Type u}
[strict_ordered_ring α]
{a b c : α}
(h : b < a)
(hc : c < 0) :
theorem
mul_pos_of_neg_of_neg
{α : Type u}
[strict_ordered_ring α]
{a b : α}
(ha : a < 0)
(hb : b < 0) :
theorem
lt_mul_of_lt_one_left
{α : Type u}
[strict_ordered_ring α]
{a b : α}
(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}
[strict_ordered_ring α]
{a b : α}
(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}
[strict_ordered_ring α]
{a b : α}
(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}
[strict_ordered_ring α]
{a b : α}
(ha : a < 0)
(h : 1 < b) :
Variant of lt_mul_of_lt_one_right for a negative instead of positive.
theorem
strict_anti_mul_right
{α : Type u}
[strict_ordered_ring α]
{a : α}
(ha : a < 0) :
strict_anti (λ (x : α), x * a)
theorem
strict_mono.const_mul_of_neg
{α : Type u}
{β : Type u_1}
[strict_ordered_ring α]
{a : α}
[preorder β]
{f : β → α}
(hf : strict_mono f)
(ha : a < 0) :
strict_anti (λ (x : β), a * f x)
theorem
strict_mono.mul_const_of_neg
{α : Type u}
{β : Type u_1}
[strict_ordered_ring α]
{a : α}
[preorder β]
{f : β → α}
(hf : strict_mono f)
(ha : a < 0) :
strict_anti (λ (x : β), f x * a)
theorem
strict_anti.const_mul_of_neg
{α : Type u}
{β : Type u_1}
[strict_ordered_ring α]
{a : α}
[preorder β]
{f : β → α}
(hf : strict_anti f)
(ha : a < 0) :
strict_mono (λ (x : β), a * f x)
theorem
strict_anti.mul_const_of_neg
{α : Type u}
{β : Type u_1}
[strict_ordered_ring α]
{a : α}
[preorder β]
{f : β → α}
(hf : strict_anti f)
(ha : a < 0) :
strict_mono (λ (x : β), f x * a)
@[reducible]
def
strict_ordered_comm_ring.to_ordered_comm_ring'
{α : Type u}
[strict_ordered_comm_ring α]
[decidable_rel has_le.le] :
A choice-free version of strict_ordered_comm_ring.to_ordered_comm_semiring' to avoid using
choice in basic int lemmas.
Equations
- strict_ordered_comm_ring.to_ordered_comm_ring' = {add := strict_ordered_comm_ring.add _inst_1, add_assoc := _, zero := strict_ordered_comm_ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := strict_ordered_comm_ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := strict_ordered_comm_ring.neg _inst_1, sub := strict_ordered_comm_ring.sub _inst_1, sub_eq_add_neg := _, zsmul := strict_ordered_comm_ring.zsmul _inst_1, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := strict_ordered_comm_ring.int_cast _inst_1, nat_cast := strict_ordered_comm_ring.nat_cast _inst_1, one := strict_ordered_comm_ring.one _inst_1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := strict_ordered_comm_ring.mul _inst_1, mul_assoc := _, one_mul := _, mul_one := _, npow := strict_ordered_comm_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := strict_ordered_comm_ring.le _inst_1, lt := strict_ordered_comm_ring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_nonneg := _, mul_comm := _}
@[protected, instance]
def
strict_ordered_comm_ring.to_strict_ordered_comm_semiring
{α : Type u}
[strict_ordered_comm_ring α] :
Equations
- strict_ordered_comm_ring.to_strict_ordered_comm_semiring = {add := strict_ordered_comm_ring.add _inst_1, add_assoc := _, zero := strict_ordered_comm_ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := strict_ordered_comm_ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := strict_ordered_comm_ring.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := strict_ordered_comm_ring.one _inst_1, one_mul := _, mul_one := _, nat_cast := strict_ordered_comm_ring.nat_cast _inst_1, nat_cast_zero := _, nat_cast_succ := _, npow := strict_ordered_comm_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, le := strict_ordered_comm_ring.le _inst_1, lt := strict_ordered_comm_ring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _, mul_comm := _}
@[protected, instance]
Equations
- strict_ordered_comm_ring.to_ordered_comm_ring = {add := strict_ordered_comm_ring.add _inst_1, add_assoc := _, zero := strict_ordered_comm_ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := strict_ordered_comm_ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := strict_ordered_comm_ring.neg _inst_1, sub := strict_ordered_comm_ring.sub _inst_1, sub_eq_add_neg := _, zsmul := strict_ordered_comm_ring.zsmul _inst_1, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := strict_ordered_comm_ring.int_cast _inst_1, nat_cast := strict_ordered_comm_ring.nat_cast _inst_1, one := strict_ordered_comm_ring.one _inst_1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := strict_ordered_comm_ring.mul _inst_1, mul_assoc := _, one_mul := _, mul_one := _, npow := strict_ordered_comm_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := strict_ordered_comm_ring.le _inst_1, lt := strict_ordered_comm_ring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_nonneg := _, mul_comm := _}
@[protected, instance]
@[protected, instance]
theorem
nonneg_of_mul_nonneg_left
{α : Type u}
[linear_ordered_semiring α]
{a b : α}
(h : 0 ≤ a * b)
(hb : 0 < b) :
0 ≤ a
theorem
nonneg_of_mul_nonneg_right
{α : Type u}
[linear_ordered_semiring α]
{a b : α}
(h : 0 ≤ a * b)
(ha : 0 < a) :
0 ≤ b
theorem
neg_of_mul_neg_left
{α : Type u}
[linear_ordered_semiring α]
{a b : α}
(h : a * b < 0)
(hb : 0 ≤ b) :
a < 0
theorem
neg_of_mul_neg_right
{α : Type u}
[linear_ordered_semiring α]
{a b : α}
(h : a * b < 0)
(ha : 0 ≤ a) :
b < 0
theorem
nonpos_of_mul_nonpos_left
{α : Type u}
[linear_ordered_semiring α]
{a b : α}
(h : a * b ≤ 0)
(hb : 0 < b) :
a ≤ 0
theorem
nonpos_of_mul_nonpos_right
{α : Type u}
[linear_ordered_semiring α]
{a b : α}
(h : a * b ≤ 0)
(ha : 0 < a) :
b ≤ 0
@[simp]
@[simp]
theorem
add_le_mul_of_left_le_right
{α : Type u}
[linear_ordered_semiring α]
{a b : α}
(a2 : 2 ≤ a)
(ab : a ≤ b) :
theorem
add_le_mul_of_right_le_left
{α : Type u}
[linear_ordered_semiring α]
{a b : α}
(b2 : 2 ≤ b)
(ba : b ≤ a) :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
mul_nonneg_iff_right_nonneg_of_pos
{α : Type u}
[linear_ordered_semiring α]
{a b : α}
(ha : 0 < a) :
theorem
mul_nonneg_iff_left_nonneg_of_pos
{α : Type u}
[linear_ordered_semiring α]
{a b : α}
(hb : 0 < b) :
theorem
nonpos_of_mul_nonneg_left
{α : Type u}
[linear_ordered_semiring α]
{a b : α}
(h : 0 ≤ a * b)
(hb : b < 0) :
a ≤ 0
theorem
nonpos_of_mul_nonneg_right
{α : Type u}
[linear_ordered_semiring α]
{a b : α}
(h : 0 ≤ a * b)
(ha : a < 0) :
b ≤ 0
theorem
mul_max_of_nonneg
{α : Type u}
[linear_ordered_semiring α]
{a : α}
(b c : α)
(ha : 0 ≤ a) :
a * linear_order.max b c = linear_order.max (a * b) (a * c)
theorem
mul_min_of_nonneg
{α : Type u}
[linear_ordered_semiring α]
{a : α}
(b c : α)
(ha : 0 ≤ a) :
a * linear_order.min b c = linear_order.min (a * b) (a * c)
theorem
max_mul_of_nonneg
{α : Type u}
[linear_ordered_semiring α]
{c : α}
(a b : α)
(hc : 0 ≤ c) :
linear_order.max a b * c = linear_order.max (a * c) (b * c)
theorem
min_mul_of_nonneg
{α : Type u}
[linear_ordered_semiring α]
{c : α}
(a b : α)
(hc : 0 ≤ c) :
linear_order.min a b * c = linear_order.min (a * c) (b * c)
theorem
le_of_mul_le_of_one_le
{α : Type u}
[linear_ordered_semiring α]
{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}
[linear_ordered_semiring α]
{a b : α}
(hb : 0 ≤ b)
(h : a * a ≤ b * b) :
a ≤ b
@[protected, instance]
def
linear_ordered_comm_semiring.to_linear_ordered_cancel_add_comm_monoid
{α : Type u}
[linear_ordered_comm_semiring α] :
Equations
- linear_ordered_comm_semiring.to_linear_ordered_cancel_add_comm_monoid = {add := linear_ordered_comm_semiring.add _inst_1, add_assoc := _, zero := linear_ordered_comm_semiring.zero _inst_1, zero_add := _, add_zero := _, nsmul := linear_ordered_comm_semiring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := linear_ordered_comm_semiring.le _inst_1, lt := linear_ordered_comm_semiring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, le_total := _, decidable_le := linear_ordered_comm_semiring.decidable_le _inst_1, decidable_eq := linear_ordered_comm_semiring.decidable_eq _inst_1, decidable_lt := linear_ordered_comm_semiring.decidable_lt _inst_1, max := linear_ordered_comm_semiring.max _inst_1, max_def := _, min := linear_ordered_comm_semiring.min _inst_1, min_def := _}
@[protected, instance]
Equations
- linear_ordered_ring.to_linear_ordered_semiring = {add := linear_ordered_ring.add _inst_1, add_assoc := _, zero := linear_ordered_ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := linear_ordered_ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := linear_ordered_ring.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := linear_ordered_ring.one _inst_1, one_mul := _, mul_one := _, nat_cast := linear_ordered_ring.nat_cast _inst_1, nat_cast_zero := _, nat_cast_succ := _, npow := linear_ordered_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, le := linear_ordered_ring.le _inst_1, lt := linear_ordered_ring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _, le_total := _, decidable_le := linear_ordered_ring.decidable_le _inst_1, decidable_eq := linear_ordered_ring.decidable_eq _inst_1, decidable_lt := linear_ordered_ring.decidable_lt _inst_1, max := linear_ordered_ring.max _inst_1, max_def := _, min := linear_ordered_ring.min _inst_1, min_def := _}
@[protected, instance]
Equations
- linear_ordered_ring.to_linear_ordered_add_comm_group = {add := linear_ordered_ring.add _inst_1, add_assoc := _, zero := linear_ordered_ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := linear_ordered_ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := linear_ordered_ring.neg _inst_1, sub := linear_ordered_ring.sub _inst_1, sub_eq_add_neg := _, zsmul := linear_ordered_ring.zsmul _inst_1, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := linear_ordered_ring.le _inst_1, lt := linear_ordered_ring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_total := _, decidable_le := linear_ordered_ring.decidable_le _inst_1, decidable_eq := linear_ordered_ring.decidable_eq _inst_1, decidable_lt := linear_ordered_ring.decidable_lt _inst_1, max := linear_ordered_ring.max _inst_1, max_def := _, min := linear_ordered_ring.min _inst_1, min_def := _}
@[protected, instance]
@[protected, instance]
Out of three elements of a linear_ordered_ring, two must have the same sign.
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
lt_of_mul_lt_mul_of_nonpos_left
{α : Type u}
[linear_ordered_ring α]
{a b c : α}
(h : c * a < c * b)
(hc : c ≤ 0) :
b < a
theorem
lt_of_mul_lt_mul_of_nonpos_right
{α : Type u}
[linear_ordered_ring α]
{a b c : α}
(h : a * c < b * c)
(hc : c ≤ 0) :
b < a
@[simp]
theorem
mul_self_le_mul_self_of_le_of_neg_le
{α : Type u}
[linear_ordered_ring α]
{x y : α}
(h₁ : x ≤ y)
(h₂ : -x ≤ y) :
theorem
nonneg_of_mul_nonpos_left
{α : Type u}
[linear_ordered_ring α]
{a b : α}
(h : a * b ≤ 0)
(hb : b < 0) :
0 ≤ a
theorem
nonneg_of_mul_nonpos_right
{α : Type u}
[linear_ordered_ring α]
{a b : α}
(h : a * b ≤ 0)
(ha : a < 0) :
0 ≤ b
theorem
pos_of_mul_neg_left
{α : Type u}
[linear_ordered_ring α]
{a b : α}
(h : a * b < 0)
(hb : b ≤ 0) :
0 < a
theorem
pos_of_mul_neg_right
{α : Type u}
[linear_ordered_ring α]
{a b : α}
(h : a * b < 0)
(ha : a ≤ 0) :
0 < b
theorem
eq_zero_of_mul_self_add_mul_self_eq_zero
{α : Type u}
[linear_ordered_ring α]
{a b : α}
(h : a * a + b * b = 0) :
a = 0
@[protected, instance]
def
linear_ordered_comm_ring.to_strict_ordered_comm_ring
{α : Type u}
[d : linear_ordered_comm_ring α] :
Equations
- linear_ordered_comm_ring.to_strict_ordered_comm_ring = {add := linear_ordered_comm_ring.add d, add_assoc := _, zero := linear_ordered_comm_ring.zero d, zero_add := _, add_zero := _, nsmul := linear_ordered_comm_ring.nsmul d, nsmul_zero' := _, nsmul_succ' := _, neg := linear_ordered_comm_ring.neg d, sub := linear_ordered_comm_ring.sub d, sub_eq_add_neg := _, zsmul := linear_ordered_comm_ring.zsmul d, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := linear_ordered_comm_ring.int_cast d, nat_cast := linear_ordered_comm_ring.nat_cast d, one := linear_ordered_comm_ring.one d, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := linear_ordered_comm_ring.mul d, mul_assoc := _, one_mul := _, mul_one := _, npow := linear_ordered_comm_ring.npow d, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := linear_ordered_comm_ring.le d, lt := linear_ordered_comm_ring.lt d, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_pos := _, mul_comm := _}
@[protected, instance]
def
linear_ordered_comm_ring.to_linear_ordered_comm_semiring
{α : Type u}
[d : linear_ordered_comm_ring α] :
Equations
- linear_ordered_comm_ring.to_linear_ordered_comm_semiring = {add := linear_ordered_comm_ring.add d, add_assoc := _, zero := linear_ordered_comm_ring.zero d, zero_add := _, add_zero := _, nsmul := linear_ordered_comm_ring.nsmul d, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := linear_ordered_comm_ring.mul d, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := linear_ordered_comm_ring.one d, one_mul := _, mul_one := _, nat_cast := linear_ordered_comm_ring.nat_cast d, nat_cast_zero := _, nat_cast_succ := _, npow := linear_ordered_comm_ring.npow d, npow_zero' := _, npow_succ' := _, le := linear_ordered_comm_ring.le d, lt := linear_ordered_comm_ring.lt d, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _, mul_comm := _, le_total := _, decidable_le := linear_ordered_comm_ring.decidable_le d, decidable_eq := linear_ordered_comm_ring.decidable_eq d, decidable_lt := linear_ordered_comm_ring.decidable_lt d, max := linear_ordered_comm_ring.max d, max_def := _, min := linear_ordered_comm_ring.min d, min_def := _}
theorem
max_mul_mul_le_max_mul_max
{α : Type u}
[linear_ordered_comm_ring α]
{a d : α}
(b c : α)
(ha : 0 ≤ a)
(hd : 0 ≤ d) :
linear_order.max (a * b) (d * c) ≤ linear_order.max a c * linear_order.max d b