Linear ordered (semi)fields #
A linear ordered (semi)field is a (semi)field equipped with a linear order such that
- addition respects the order:
a ≤ b → c + a ≤ c + b
; - multiplication of positives is positive:
0 < a → 0 < b → 0 < a * b
; 0 < 1
.
Main Definitions #
LinearOrderedSemifield
: Typeclass for linear order semifields.LinearOrderedField
: Typeclass for linear ordered fields.
A linear ordered semifield is a field with a linear order respecting the operations.
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
- one : α
- natCast : ℕ → α
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow : ℕ → α → α
- npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y
- zero_le_one : 0 ≤ 1
- min : α → α → α
- max : α → α → α
- compare : α → α → Ordering
- decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
- decidableEq : DecidableEq α
- decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
- compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
- inv : α → α
- div : α → α → α
a / b := a * b⁻¹
- zpow : ℤ → α → α
The power operation:
a ^ n = a * ··· * a
;a ^ (-n) = a⁻¹ * ··· a⁻¹
(n
times) - zpow_zero' : ∀ (a : α), LinearOrderedSemifield.zpow 0 a = 1
a ^ 0 = 1
- zpow_succ' : ∀ (n : ℕ) (a : α), LinearOrderedSemifield.zpow (Int.ofNat n.succ) a = LinearOrderedSemifield.zpow (Int.ofNat n) a * a
a ^ (n + 1) = a ^ n * a
- zpow_neg' : ∀ (n : ℕ) (a : α), LinearOrderedSemifield.zpow (Int.negSucc n) a = (LinearOrderedSemifield.zpow (↑n.succ) a)⁻¹
a ^ -(n + 1) = (a ^ (n + 1))⁻¹
The inverse of
0
in a group with zero is0
.Every nonzero element of a group with zero is invertible.
- nnratCast : ℚ≥0 → α
However
NNRat.cast
is defined, it must be propositionally equal toa / b
.Do not use this lemma directly. Use
NNRat.cast_def
instead.- nnqsmul : ℚ≥0 → α → α
Scalar multiplication by a nonnegative rational number.
Unless there is a risk of a
Module ℚ≥0 _
instance diamond, writennqsmul := _
. This will setnnqsmul
to(NNRat.cast · * ·)
thanks to unification in the default proof ofnnqsmul_def
.Do not use directly. Instead use the
•
notation. - nnqsmul_def : ∀ (q : ℚ≥0) (a : α), LinearOrderedSemifield.nnqsmul q a = ↑q * a
However
qsmul
is defined, it must be propositionally equal to multiplication byRat.cast
.Do not use this lemma directly. Use
NNRat.smul_def
instead.
Instances
A linear ordered field is a field with a linear order respecting the operations.
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
- one : α
- natCast : ℕ → α
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow : ℕ → α → α
- npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
- intCast : ℤ → α
- intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
- intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y
- zero_le_one : 0 ≤ 1
- min : α → α → α
- max : α → α → α
- compare : α → α → Ordering
- decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
- decidableEq : DecidableEq α
- decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
- compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
- inv : α → α
- div : α → α → α
a / b := a * b⁻¹
- zpow : ℤ → α → α
The power operation:
a ^ n = a * ··· * a
;a ^ (-n) = a⁻¹ * ··· a⁻¹
(n
times) - zpow_zero' : ∀ (a : α), LinearOrderedField.zpow 0 a = 1
a ^ 0 = 1
- zpow_succ' : ∀ (n : ℕ) (a : α), LinearOrderedField.zpow (Int.ofNat n.succ) a = LinearOrderedField.zpow (Int.ofNat n) a * a
a ^ (n + 1) = a ^ n * a
- zpow_neg' : ∀ (n : ℕ) (a : α), LinearOrderedField.zpow (Int.negSucc n) a = (LinearOrderedField.zpow (↑n.succ) a)⁻¹
a ^ -(n + 1) = (a ^ (n + 1))⁻¹
- nnratCast : ℚ≥0 → α
- ratCast : ℚ → α
For a nonzero
a
,a⁻¹
is a right multiplicative inverse.The inverse of
0
is0
by convention.However
NNRat.cast
is defined, it must be equal toa / b
.Do not use this lemma directly. Use
NNRat.cast_def
instead.- nnqsmul : ℚ≥0 → α → α
Scalar multiplication by a nonnegative rational number.
Unless there is a risk of a
Module ℚ≥0 _
instance diamond, writennqsmul := _
. This will setnnqsmul
to(NNRat.cast · * ·)
thanks to unification in the default proof ofnnqsmul_def
.Do not use directly. Instead use the
•
notation. - nnqsmul_def : ∀ (q : ℚ≥0) (a : α), LinearOrderedField.nnqsmul q a = ↑q * a
However
qsmul
is defined, it must be propositionally equal to multiplication byRat.cast
.Do not use this lemma directly. Use
NNRat.smul_def
instead. However
Rat.cast q
is defined, it must be propositionally equal toq.num / q.den
.Do not use this lemma directly. Use
Rat.cast_def
instead.- qsmul : ℚ → α → α
Scalar multiplication by a rational number.
Unless there is a risk of a
Module ℚ _
instance diamond, writeqsmul := _
. This will setqsmul
to(Rat.cast · * ·)
thanks to unification in the default proof ofqsmul_def
.Do not use directly. Instead use the
•
notation. - qsmul_def : ∀ (a : ℚ) (x : α), LinearOrderedField.qsmul a x = ↑a * x
However
qsmul
is defined, it must be propositionally equal to multiplication byRat.cast
.Do not use this lemma directly. Use
Rat.cast_def
instead.
Instances
Equations
- LinearOrderedField.toLinearOrderedSemifield = LinearOrderedSemifield.mk ⋯ LinearOrderedField.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ LinearOrderedField.nnqsmul ⋯
Equality holds when a ≠ 0
. See mul_inv_cancel
.
Equality holds when a ≠ 0
. See inv_mul_cancel
.
Equality holds when a ≠ 0
. See mul_inv_cancel_left
.
Equality holds when a ≠ 0
. See mul_inv_cancel_left
.
Equality holds when a ≠ 0
. See inv_mul_cancel_left
.
Equality holds when a ≠ 0
. See inv_mul_cancel_left
.
Equality holds when b ≠ 0
. See mul_inv_cancel_right
.
Equality holds when b ≠ 0
. See mul_inv_cancel_right
.
Equality holds when b ≠ 0
. See inv_mul_cancel_right
.
Equality holds when b ≠ 0
. See inv_mul_cancel_right
.