- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- 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 : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- 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"
- zero_mul : ∀ (a : α), 0 * a = 0
- mul_zero : ∀ (a : α), a * 0 = 0
- left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
- add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1 → b = c_1
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
- 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_1 : α), c_1 + a ≤ c_1 + b
- le_of_add_le_add_left : ∀ (a b c_1 : α), a + b ≤ a + c_1 → b ≤ c_1
- zero_le_one : 0 ≤ 1
- mul_lt_mul_of_pos_left : ∀ (a b c_1 : α), a < b → 0 < c_1 → c_1 * a < c_1 * b
- mul_lt_mul_of_pos_right : ∀ (a b c_1 : α), a < b → 0 < c_1 → a * c_1 < b * c_1
An ordered_semiring α
is a semiring α
with a partial order such that
multiplication with a positive number and addition are monotone.
Pullback an ordered_semiring
under an injective map.
Equations
- function.injective.ordered_semiring f hf zero one add mul = {add := ordered_cancel_add_comm_monoid.add (function.injective.ordered_cancel_add_comm_monoid f hf zero add), add_assoc := _, zero := ordered_cancel_add_comm_monoid.zero (function.injective.ordered_cancel_add_comm_monoid f hf zero add), zero_add := _, add_zero := _, nsmul := ordered_cancel_add_comm_monoid.nsmul (function.injective.ordered_cancel_add_comm_monoid f hf zero add), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul (function.injective.semiring f hf zero one add mul), mul_assoc := _, one := semiring.one (function.injective.semiring f hf zero one add mul), one_mul := _, mul_one := _, npow := semiring.npow (function.injective.semiring f hf zero one add mul), npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, add_left_cancel := _, le := ordered_cancel_add_comm_monoid.le (function.injective.ordered_cancel_add_comm_monoid f hf zero add), lt := ordered_cancel_add_comm_monoid.lt (function.injective.ordered_cancel_add_comm_monoid f hf zero add), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _}
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- 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 : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- 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"
- zero_mul : ∀ (a : α), 0 * a = 0
- mul_zero : ∀ (a : α), a * 0 = 0
- left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
- add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1 → b = c_1
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
- 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_1 : α), c_1 + a ≤ c_1 + b
- le_of_add_le_add_left : ∀ (a b c_1 : α), a + b ≤ a + c_1 → b ≤ c_1
- zero_le_one : 0 ≤ 1
- mul_lt_mul_of_pos_left : ∀ (a b c_1 : α), a < b → 0 < c_1 → c_1 * a < c_1 * b
- mul_lt_mul_of_pos_right : ∀ (a b c_1 : α), a < b → 0 < c_1 → a * c_1 < b * c_1
- mul_comm : ∀ (a b : α), a * b = b * a
An ordered_comm_semiring α
is a commutative semiring α
with a partial order such that
multiplication with a positive number and addition are monotone.
Pullback an ordered_comm_semiring
under an injective map.
Equations
- function.injective.ordered_comm_semiring f hf zero one add mul = {add := comm_semiring.add (function.injective.comm_semiring f hf zero one add mul), add_assoc := _, zero := comm_semiring.zero (function.injective.comm_semiring f hf zero one add mul), zero_add := _, add_zero := _, nsmul := comm_semiring.nsmul (function.injective.comm_semiring f hf zero one add mul), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_semiring.mul (function.injective.comm_semiring f hf zero one add mul), mul_assoc := _, one := comm_semiring.one (function.injective.comm_semiring f hf zero one add mul), one_mul := _, mul_one := _, npow := comm_semiring.npow (function.injective.comm_semiring f hf zero one add mul), npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, add_left_cancel := _, le := ordered_semiring.le (function.injective.ordered_semiring f hf zero one add mul), lt := ordered_semiring.lt (function.injective.ordered_semiring f hf zero one add mul), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _, mul_comm := _}
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- 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 : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- 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"
- zero_mul : ∀ (a : α), 0 * a = 0
- mul_zero : ∀ (a : α), a * 0 = 0
- left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
- add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1 → b = c_1
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
- 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_1 : α), c_1 + a ≤ c_1 + b
- le_of_add_le_add_left : ∀ (a b c_1 : α), a + b ≤ a + c_1 → b ≤ c_1
- zero_le_one : 0 ≤ 1
- mul_lt_mul_of_pos_left : ∀ (a b c_1 : α), a < b → 0 < c_1 → c_1 * a < c_1 * b
- mul_lt_mul_of_pos_right : ∀ (a b c_1 : α), a < b → 0 < c_1 → a * c_1 < b * c_1
- 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
- exists_pair_ne : ∃ (x y : α), x ≠ y
A linear_ordered_semiring α
is a nontrivial semiring α
with a linear order
such that multiplication with a positive number and addition are monotone.
Instances
- linear_ordered_ring.to_linear_ordered_semiring
- linear_ordered_comm_ring.to_linear_ordered_semiring
- nat.linear_ordered_semiring
- rat.linear_ordered_semiring
- subsemiring.to_linear_ordered_semiring
- subalgebra.to_linear_ordered_semiring
- real.linear_ordered_semiring
- nnreal.linear_ordered_semiring
- num.linear_ordered_semiring
- zsqrtd.linear_ordered_semiring
Pullback a linear_ordered_semiring
under an injective map.
Equations
- function.injective.linear_ordered_semiring f hf zero one add mul = {add := ordered_semiring.add (function.injective.ordered_semiring f hf zero one add mul), add_assoc := _, zero := ordered_semiring.zero (function.injective.ordered_semiring f hf zero one add mul), zero_add := _, add_zero := _, nsmul := ordered_semiring.nsmul (function.injective.ordered_semiring f hf zero one add mul), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := ordered_semiring.mul (function.injective.ordered_semiring f hf zero one add mul), mul_assoc := _, one := ordered_semiring.one (function.injective.ordered_semiring f hf zero one add mul), one_mul := _, mul_one := _, npow := ordered_semiring.npow (function.injective.ordered_semiring f hf zero one add mul), npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, add_left_cancel := _, le := linear_order.le (linear_order.lift f hf), lt := linear_order.lt (linear_order.lift f hf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _, le_total := _, decidable_le := linear_order.decidable_le (linear_order.lift f hf), decidable_eq := linear_order.decidable_eq (linear_order.lift f hf), decidable_lt := linear_order.decidable_lt (linear_order.lift f hf), exists_pair_ne := _}
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- 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"
- gsmul : ℤ → α → α
- gsmul_zero' : (∀ (a : α), ordered_ring.gsmul 0 a = 0) . "try_refl_tac"
- gsmul_succ' : (∀ (n : ℕ) (a : α), ordered_ring.gsmul (int.of_nat n.succ) a = a + ordered_ring.gsmul (int.of_nat n) a) . "try_refl_tac"
- gsmul_neg' : (∀ (n : ℕ) (a : α), ordered_ring.gsmul -[1+ n] a = -ordered_ring.gsmul ↑(n.succ) a) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- 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_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
- 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_1 : α), c_1 + a ≤ c_1 + b
- zero_le_one : 0 ≤ 1
- mul_pos : ∀ (a b : α), 0 < a → 0 < b → 0 < a * b
An ordered_ring α
is a ring α
with a partial order such that
multiplication with a positive number and addition are monotone.
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, mul_assoc := _, one := ordered_ring.one _inst_1, one_mul := _, mul_one := _, npow := ordered_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, add_left_cancel := _, 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 := _, le_of_add_le_add_left := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _}
Pullback an ordered_ring
under an injective map.
Equations
- function.injective.ordered_ring f hf zero one add mul neg sub = {add := ordered_semiring.add (function.injective.ordered_semiring f hf zero one add mul), add_assoc := _, zero := ordered_semiring.zero (function.injective.ordered_semiring f hf zero one add mul), zero_add := _, add_zero := _, nsmul := ordered_semiring.nsmul (function.injective.ordered_semiring f hf zero one add mul), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (function.injective.ring f hf zero one add mul neg sub), sub := ring.sub (function.injective.ring f hf zero one add mul neg sub), sub_eq_add_neg := _, gsmul := ring.gsmul (function.injective.ring f hf zero one add mul neg sub), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ordered_semiring.mul (function.injective.ordered_semiring f hf zero one add mul), mul_assoc := _, one := ordered_semiring.one (function.injective.ordered_semiring f hf zero one add mul), one_mul := _, mul_one := _, npow := ordered_semiring.npow (function.injective.ordered_semiring f hf zero one add mul), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := ordered_semiring.le (function.injective.ordered_semiring f hf zero one add mul), lt := ordered_semiring.lt (function.injective.ordered_semiring f hf zero one add mul), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _}
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- 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"
- gsmul : ℤ → α → α
- gsmul_zero' : (∀ (a : α), ordered_comm_ring.gsmul 0 a = 0) . "try_refl_tac"
- gsmul_succ' : (∀ (n : ℕ) (a : α), ordered_comm_ring.gsmul (int.of_nat n.succ) a = a + ordered_comm_ring.gsmul (int.of_nat n) a) . "try_refl_tac"
- gsmul_neg' : (∀ (n : ℕ) (a : α), ordered_comm_ring.gsmul -[1+ n] a = -ordered_comm_ring.gsmul ↑(n.succ) a) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- 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_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
- 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_1 : α), c_1 + a ≤ c_1 + b
- zero_le_one : 0 ≤ 1
- mul_pos : ∀ (a b : α), 0 < a → 0 < b → 0 < a * b
- zero_mul : ∀ (a : α), 0 * a = 0
- mul_zero : ∀ (a : α), a * 0 = 0
- add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1 → b = c_1
- le_of_add_le_add_left : ∀ (a b c_1 : α), a + b ≤ a + c_1 → b ≤ c_1
- mul_lt_mul_of_pos_left : ∀ (a b c_1 : α), a < b → 0 < c_1 → c_1 * a < c_1 * b
- mul_lt_mul_of_pos_right : ∀ (a b c_1 : α), a < b → 0 < c_1 → a * c_1 < b * c_1
- mul_comm : ∀ (a b : α), a * b = b * a
An ordered_comm_ring α
is a commutative ring α
with a partial order such that
multiplication with a positive number and addition are monotone.
Pullback an ordered_comm_ring
under an injective map.
Equations
- function.injective.ordered_comm_ring f hf zero one add mul neg sub = {add := ordered_comm_semiring.add (function.injective.ordered_comm_semiring f hf zero one add mul), add_assoc := _, zero := ordered_comm_semiring.zero (function.injective.ordered_comm_semiring f hf zero one add mul), zero_add := _, add_zero := _, nsmul := ordered_comm_semiring.nsmul (function.injective.ordered_comm_semiring f hf zero one add mul), nsmul_zero' := _, nsmul_succ' := _, neg := ordered_ring.neg (function.injective.ordered_ring f hf zero one add mul neg sub), sub := ordered_ring.sub (function.injective.ordered_ring f hf zero one add mul neg sub), sub_eq_add_neg := _, gsmul := ordered_ring.gsmul (function.injective.ordered_ring f hf zero one add mul neg sub), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ordered_comm_semiring.mul (function.injective.ordered_comm_semiring f hf zero one add mul), mul_assoc := _, one := ordered_comm_semiring.one (function.injective.ordered_comm_semiring f hf zero one add mul), one_mul := _, mul_one := _, npow := ordered_comm_semiring.npow (function.injective.ordered_comm_semiring f hf zero one add mul), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := ordered_comm_semiring.le (function.injective.ordered_comm_semiring f hf zero one add mul), lt := ordered_comm_semiring.lt (function.injective.ordered_comm_semiring f hf zero one add mul), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _, zero_mul := _, mul_zero := _, add_left_cancel := _, le_of_add_le_add_left := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _, mul_comm := _}
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- 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"
- gsmul : ℤ → α → α
- gsmul_zero' : (∀ (a : α), linear_ordered_ring.gsmul 0 a = 0) . "try_refl_tac"
- gsmul_succ' : (∀ (n : ℕ) (a : α), linear_ordered_ring.gsmul (int.of_nat n.succ) a = a + linear_ordered_ring.gsmul (int.of_nat n) a) . "try_refl_tac"
- gsmul_neg' : (∀ (n : ℕ) (a : α), linear_ordered_ring.gsmul -[1+ n] a = -linear_ordered_ring.gsmul ↑(n.succ) a) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- 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_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
- 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_1 : α), c_1 + a ≤ c_1 + b
- 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
- exists_pair_ne : ∃ (x y : α), x ≠ y
A linear_ordered_ring α
is a ring α
with a linear order such that
multiplication with a positive number and addition are monotone.
Equations
- linear_ordered_ring.to_linear_ordered_add_comm_group = {add := linear_ordered_ring.add s, add_assoc := _, zero := linear_ordered_ring.zero s, zero_add := _, add_zero := _, nsmul := linear_ordered_ring.nsmul s, nsmul_zero' := _, nsmul_succ' := _, neg := linear_ordered_ring.neg s, sub := linear_ordered_ring.sub s, sub_eq_add_neg := _, gsmul := linear_ordered_ring.gsmul s, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, le := linear_ordered_ring.le s, lt := linear_ordered_ring.lt s, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_ordered_ring.decidable_le s, decidable_eq := linear_ordered_ring.decidable_eq s, decidable_lt := linear_ordered_ring.decidable_lt s, add_le_add_left := _}
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, mul_assoc := _, one := linear_ordered_ring.one _inst_1, one_mul := _, mul_one := _, npow := linear_ordered_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, add_left_cancel := _, 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 := _, 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, exists_pair_ne := _}
Equations
- linear_ordered_ring.to_domain = {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 := _, gsmul := linear_ordered_ring.gsmul _inst_1, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := linear_ordered_ring.mul _inst_1, mul_assoc := _, one := linear_ordered_ring.one _inst_1, one_mul := _, mul_one := _, npow := linear_ordered_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
abs
as a monoid_with_zero_hom
.
Pullback a linear_ordered_ring
under an injective map.
Equations
- function.injective.linear_ordered_ring f hf zero one add mul neg sub = {add := ordered_ring.add (function.injective.ordered_ring f hf zero one add mul neg sub), add_assoc := _, zero := ordered_ring.zero (function.injective.ordered_ring f hf zero one add mul neg sub), zero_add := _, add_zero := _, nsmul := ordered_ring.nsmul (function.injective.ordered_ring f hf zero one add mul neg sub), nsmul_zero' := _, nsmul_succ' := _, neg := ordered_ring.neg (function.injective.ordered_ring f hf zero one add mul neg sub), sub := ordered_ring.sub (function.injective.ordered_ring f hf zero one add mul neg sub), sub_eq_add_neg := _, gsmul := ordered_ring.gsmul (function.injective.ordered_ring f hf zero one add mul neg sub), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ordered_ring.mul (function.injective.ordered_ring f hf zero one add mul neg sub), mul_assoc := _, one := ordered_ring.one (function.injective.ordered_ring f hf zero one add mul neg sub), one_mul := _, mul_one := _, npow := ordered_ring.npow (function.injective.ordered_ring f hf zero one add mul neg sub), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := linear_order.le (linear_order.lift f hf), lt := linear_order.lt (linear_order.lift f hf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_order.decidable_le (linear_order.lift f hf), decidable_eq := linear_order.decidable_eq (linear_order.lift f hf), decidable_lt := linear_order.decidable_lt (linear_order.lift f hf), exists_pair_ne := _}
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- 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"
- gsmul : ℤ → α → α
- gsmul_zero' : (∀ (a : α), linear_ordered_comm_ring.gsmul 0 a = 0) . "try_refl_tac"
- gsmul_succ' : (∀ (n : ℕ) (a : α), linear_ordered_comm_ring.gsmul (int.of_nat n.succ) a = a + linear_ordered_comm_ring.gsmul (int.of_nat n) a) . "try_refl_tac"
- gsmul_neg' : (∀ (n : ℕ) (a : α), linear_ordered_comm_ring.gsmul -[1+ n] a = -linear_ordered_comm_ring.gsmul ↑(n.succ) a) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- 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_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
- 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_1 : α), c_1 + a ≤ c_1 + b
- 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
- exists_pair_ne : ∃ (x y : α), x ≠ y
- mul_comm : ∀ (a b : α), a * b = b * a
A linear_ordered_comm_ring α
is a commutative ring α
with a linear order
such that multiplication with a positive number and addition are monotone.
Instances
- linear_ordered_field.to_linear_ordered_comm_ring
- int.linear_ordered_comm_ring
- rat.linear_ordered_comm_ring
- subring.to_linear_ordered_comm_ring
- subalgebra.to_linear_ordered_comm_ring
- real.linear_ordered_comm_ring
- znum.linear_ordered_comm_ring
- filter.germ.linear_ordered_comm_ring
- zsqrtd.linear_ordered_comm_ring
Equations
- linear_ordered_comm_ring.to_ordered_comm_ring = let s : linear_ordered_semiring α := linear_ordered_ring.to_linear_ordered_semiring in {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 := _, gsmul := linear_ordered_comm_ring.gsmul d, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := linear_ordered_comm_ring.mul d, mul_assoc := _, one := linear_ordered_comm_ring.one d, 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 := _, zero_le_one := _, mul_pos := _, zero_mul := _, mul_zero := _, add_left_cancel := _, le_of_add_le_add_left := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _, mul_comm := _}
Equations
- linear_ordered_comm_ring.to_integral_domain = {add := domain.add linear_ordered_ring.to_domain, add_assoc := _, zero := domain.zero linear_ordered_ring.to_domain, zero_add := _, add_zero := _, nsmul := domain.nsmul linear_ordered_ring.to_domain, nsmul_zero' := _, nsmul_succ' := _, neg := domain.neg linear_ordered_ring.to_domain, sub := domain.sub linear_ordered_ring.to_domain, sub_eq_add_neg := _, gsmul := domain.gsmul linear_ordered_ring.to_domain, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := domain.mul linear_ordered_ring.to_domain, mul_assoc := _, one := domain.one linear_ordered_ring.to_domain, one_mul := _, mul_one := _, npow := domain.npow linear_ordered_ring.to_domain, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
Equations
- linear_ordered_comm_ring.to_linear_ordered_semiring = let s : linear_ordered_semiring α := linear_ordered_ring.to_linear_ordered_semiring in {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, mul_assoc := _, one := linear_ordered_comm_ring.one d, one_mul := _, mul_one := _, npow := linear_ordered_comm_ring.npow d, npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, add_left_cancel := _, 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 := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _, 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, exists_pair_ne := _}
Pullback a linear_ordered_comm_ring
under an injective map.
Equations
- function.injective.linear_ordered_comm_ring f hf zero one add mul neg sub = {add := ordered_comm_ring.add (function.injective.ordered_comm_ring f hf zero one add mul neg sub), add_assoc := _, zero := ordered_comm_ring.zero (function.injective.ordered_comm_ring f hf zero one add mul neg sub), zero_add := _, add_zero := _, nsmul := ordered_comm_ring.nsmul (function.injective.ordered_comm_ring f hf zero one add mul neg sub), nsmul_zero' := _, nsmul_succ' := _, neg := ordered_comm_ring.neg (function.injective.ordered_comm_ring f hf zero one add mul neg sub), sub := ordered_comm_ring.sub (function.injective.ordered_comm_ring f hf zero one add mul neg sub), sub_eq_add_neg := _, gsmul := ordered_comm_ring.gsmul (function.injective.ordered_comm_ring f hf zero one add mul neg sub), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ordered_comm_ring.mul (function.injective.ordered_comm_ring f hf zero one add mul neg sub), mul_assoc := _, one := ordered_comm_ring.one (function.injective.ordered_comm_ring f hf zero one add mul neg sub), one_mul := _, mul_one := _, npow := ordered_comm_ring.npow (function.injective.ordered_comm_ring f hf zero one add mul neg sub), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := linear_order.le (linear_order.lift f hf), lt := linear_order.lt (linear_order.lift f hf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_order.decidable_le (linear_order.lift f hf), decidable_eq := linear_order.decidable_eq (linear_order.lift f hf), decidable_lt := linear_order.decidable_lt (linear_order.lift f hf), exists_pair_ne := _, mul_comm := _}
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), nonneg_ring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), nonneg_ring.nsmul n.succ x = x + nonneg_ring.nsmul n x) . "try_refl_tac"
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
- gsmul : ℤ → α → α
- gsmul_zero' : (∀ (a : α), nonneg_ring.gsmul 0 a = 0) . "try_refl_tac"
- gsmul_succ' : (∀ (n : ℕ) (a : α), nonneg_ring.gsmul (int.of_nat n.succ) a = a + nonneg_ring.gsmul (int.of_nat n) a) . "try_refl_tac"
- gsmul_neg' : (∀ (n : ℕ) (a : α), nonneg_ring.gsmul -[1+ n] a = -nonneg_ring.gsmul ↑(n.succ) a) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), nonneg_ring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), nonneg_ring.npow n.succ x = x * nonneg_ring.npow n x) . "try_refl_tac"
- left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
- nonneg : α → Prop
- pos : α → Prop
- pos_iff : (∀ (a : α), nonneg_ring.pos a ↔ nonneg_ring.nonneg a ∧ ¬nonneg_ring.nonneg (-a)) . "order_laws_tac"
- zero_nonneg : nonneg_ring.nonneg 0
- add_nonneg : ∀ {a b : α}, nonneg_ring.nonneg a → nonneg_ring.nonneg b → nonneg_ring.nonneg (a + b)
- nonneg_antisymm : ∀ {a : α}, nonneg_ring.nonneg a → nonneg_ring.nonneg (-a) → a = 0
- one_nonneg : nonneg_ring.nonneg 1
- mul_nonneg : ∀ {a b : α}, nonneg_ring.nonneg a → nonneg_ring.nonneg b → nonneg_ring.nonneg (a * b)
- mul_pos : ∀ {a b : α}, nonneg_ring.pos a → nonneg_ring.pos b → nonneg_ring.pos (a * b)
Extend nonneg_add_comm_group
to support ordered rings
specified by their nonnegative elements
Instances
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), linear_nonneg_ring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), linear_nonneg_ring.nsmul n.succ x = x + linear_nonneg_ring.nsmul n x) . "try_refl_tac"
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
- gsmul : ℤ → α → α
- gsmul_zero' : (∀ (a : α), linear_nonneg_ring.gsmul 0 a = 0) . "try_refl_tac"
- gsmul_succ' : (∀ (n : ℕ) (a : α), linear_nonneg_ring.gsmul (int.of_nat n.succ) a = a + linear_nonneg_ring.gsmul (int.of_nat n) a) . "try_refl_tac"
- gsmul_neg' : (∀ (n : ℕ) (a : α), linear_nonneg_ring.gsmul -[1+ n] a = -linear_nonneg_ring.gsmul ↑(n.succ) a) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), linear_nonneg_ring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), linear_nonneg_ring.npow n.succ x = x * linear_nonneg_ring.npow n x) . "try_refl_tac"
- left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
- exists_pair_ne : ∃ (x y : α), x ≠ y
- eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : α), a * b = 0 → a = 0 ∨ b = 0
- nonneg : α → Prop
- pos : α → Prop
- pos_iff : (∀ (a : α), linear_nonneg_ring.pos a ↔ linear_nonneg_ring.nonneg a ∧ ¬linear_nonneg_ring.nonneg (-a)) . "order_laws_tac"
- zero_nonneg : linear_nonneg_ring.nonneg 0
- add_nonneg : ∀ {a b : α}, linear_nonneg_ring.nonneg a → linear_nonneg_ring.nonneg b → linear_nonneg_ring.nonneg (a + b)
- nonneg_antisymm : ∀ {a : α}, linear_nonneg_ring.nonneg a → linear_nonneg_ring.nonneg (-a) → a = 0
- one_pos : linear_nonneg_ring.pos 1
- mul_nonneg : ∀ {a b : α}, linear_nonneg_ring.nonneg a → linear_nonneg_ring.nonneg b → linear_nonneg_ring.nonneg (a * b)
- nonneg_total : ∀ (a : α), linear_nonneg_ring.nonneg a ∨ linear_nonneg_ring.nonneg (-a)
- dec_nonneg : decidable_pred linear_nonneg_ring.nonneg
Extend nonneg_add_comm_group
to support linearly ordered rings
specified by their nonnegative elements
to_linear_nonneg_ring
shows that a nonneg_ring
with a total order is a domain
,
hence a linear_nonneg_ring
.
Equations
- nonneg_ring.to_linear_nonneg_ring nonneg_total = linear_nonneg_ring.mk nonneg_ring.add nonneg_ring.add_assoc nonneg_ring.zero nonneg_ring.zero_add nonneg_ring.add_zero nonneg_ring.nsmul nonneg_ring.nsmul_zero' nonneg_ring.nsmul_succ' nonneg_ring.neg nonneg_ring.sub nonneg_ring.sub_eq_add_neg nonneg_ring.gsmul nonneg_ring.gsmul_zero' nonneg_ring.gsmul_succ' nonneg_ring.gsmul_neg' nonneg_ring.add_left_neg nonneg_ring.add_comm nonneg_ring.mul nonneg_ring.mul_assoc nonneg_ring.one nonneg_ring.one_mul nonneg_ring.mul_one nonneg_ring.npow nonneg_ring.npow_zero' nonneg_ring.npow_succ' nonneg_ring.left_distrib nonneg_ring.right_distrib nontrivial.exists_pair_ne _ nonneg_ring.nonneg nonneg_ring.pos nonneg_ring.pos_iff nonneg_ring.zero_nonneg nonneg_ring.add_nonneg nonneg_ring.nonneg_antisymm _ nonneg_ring.mul_nonneg nonneg_total
Equations
- linear_nonneg_ring.to_nonneg_ring = {add := linear_nonneg_ring.add _inst_1, add_assoc := _, zero := linear_nonneg_ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := linear_nonneg_ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := linear_nonneg_ring.neg _inst_1, sub := linear_nonneg_ring.sub _inst_1, sub_eq_add_neg := _, gsmul := linear_nonneg_ring.gsmul _inst_1, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := linear_nonneg_ring.mul _inst_1, mul_assoc := _, one := linear_nonneg_ring.one _inst_1, one_mul := _, mul_one := _, npow := linear_nonneg_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, nonneg := linear_nonneg_ring.nonneg _inst_1, pos := linear_nonneg_ring.pos _inst_1, pos_iff := _, zero_nonneg := _, add_nonneg := _, nonneg_antisymm := _, one_nonneg := _, mul_nonneg := _, mul_pos := _}
Construct linear_order
from linear_nonneg_ring
. This is not an instance
because we don't use it in mathlib
.
Equations
- linear_nonneg_ring.to_linear_order = {le := ordered_add_comm_group.le infer_instance, lt := ordered_add_comm_group.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (a b : α), _inst_2 (b - a), decidable_eq := decidable_eq_of_decidable_le (λ (a b : α), _inst_2 (b - a)), decidable_lt := λ (a b : α), decidable_lt_of_decidable_le a b}
Construct linear_ordered_ring
from linear_nonneg_ring
.
This is not an instance because we don't use it in mathlib
.
Equations
- linear_nonneg_ring.to_linear_ordered_ring = {add := linear_nonneg_ring.add _inst_1, add_assoc := _, zero := linear_nonneg_ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := linear_nonneg_ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := linear_nonneg_ring.neg _inst_1, sub := linear_nonneg_ring.sub _inst_1, sub_eq_add_neg := _, gsmul := linear_nonneg_ring.gsmul _inst_1, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := linear_nonneg_ring.mul _inst_1, mul_assoc := _, one := linear_nonneg_ring.one _inst_1, one_mul := _, mul_one := _, npow := linear_nonneg_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := ordered_add_comm_group.le infer_instance, lt := ordered_add_comm_group.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_order.decidable_le infer_instance, decidable_eq := linear_order.decidable_eq infer_instance, decidable_lt := linear_order.decidable_lt infer_instance, exists_pair_ne := _}
Convert a linear_nonneg_ring
with a commutative multiplication and
decidable non-negativity into a linear_ordered_comm_ring
Equations
- linear_nonneg_ring.to_linear_ordered_comm_ring = {add := linear_ordered_ring.add linear_nonneg_ring.to_linear_ordered_ring, add_assoc := _, zero := linear_ordered_ring.zero linear_nonneg_ring.to_linear_ordered_ring, zero_add := _, add_zero := _, nsmul := linear_ordered_ring.nsmul linear_nonneg_ring.to_linear_ordered_ring, nsmul_zero' := _, nsmul_succ' := _, neg := linear_ordered_ring.neg linear_nonneg_ring.to_linear_ordered_ring, sub := linear_ordered_ring.sub linear_nonneg_ring.to_linear_ordered_ring, sub_eq_add_neg := _, gsmul := linear_ordered_ring.gsmul linear_nonneg_ring.to_linear_ordered_ring, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := linear_ordered_ring.mul linear_nonneg_ring.to_linear_ordered_ring, mul_assoc := _, one := linear_ordered_ring.one linear_nonneg_ring.to_linear_ordered_ring, one_mul := _, mul_one := _, npow := linear_ordered_ring.npow linear_nonneg_ring.to_linear_ordered_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := linear_ordered_ring.le linear_nonneg_ring.to_linear_ordered_ring, lt := linear_ordered_ring.lt linear_nonneg_ring.to_linear_ordered_ring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_ordered_ring.decidable_le linear_nonneg_ring.to_linear_ordered_ring, decidable_eq := linear_ordered_ring.decidable_eq linear_nonneg_ring.to_linear_ordered_ring, decidable_lt := linear_ordered_ring.decidable_lt linear_nonneg_ring.to_linear_ordered_ring, exists_pair_ne := _, mul_comm := _}
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), canonically_ordered_comm_semiring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), canonically_ordered_comm_semiring.nsmul n.succ x = x + canonically_ordered_comm_semiring.nsmul n x) . "try_refl_tac"
- add_comm : ∀ (a b : α), a + b = b + a
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
- 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_1 : α), c_1 + a ≤ c_1 + b
- lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1
- bot : α
- bot_le : ∀ (a : α), ⊥ ≤ a
- le_iff_exists_add : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a + c_1
- mul : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), canonically_ordered_comm_semiring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), canonically_ordered_comm_semiring.npow n.succ x = x * canonically_ordered_comm_semiring.npow n x) . "try_refl_tac"
- zero_mul : ∀ (a : α), 0 * a = 0
- mul_zero : ∀ (a : α), a * 0 = 0
- left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
- mul_comm : ∀ (a b : α), a * b = b * a
- eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : α), a * b = 0 → a = 0 ∨ b = 0
A canonically ordered commutative semiring is an ordered, commutative semiring
in which a ≤ b
iff there exists c
with b = a + c
. This is satisfied by the
natural numbers, for example, but not the integers or other ordered groups.
A version of zero_lt_one : 0 < 1
for a canonically_ordered_comm_semiring
.
Equations
- with_top.canonically_ordered_comm_semiring = {add := add_comm_monoid.add with_top.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero with_top.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul with_top.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := canonically_ordered_add_monoid.le with_top.canonically_ordered_add_monoid, lt := canonically_ordered_add_monoid.lt with_top.canonically_ordered_add_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, bot := canonically_ordered_add_monoid.bot with_top.canonically_ordered_add_monoid, bot_le := _, le_iff_exists_add := _, mul := mul_zero_class.mul with_top.mul_zero_class, mul_assoc := _, one := ↑1, one_mul := _, mul_one := _, npow := comm_semiring.npow._default ↑1 mul_zero_class.mul with_top.canonically_ordered_comm_semiring._proof_18 with_top.canonically_ordered_comm_semiring._proof_19, npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}