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.
Implementation details #
For olean caching reasons, this file is separate to the main file,
Mathlib.Algebra.Order.Field.Basic
. The lemmata are instead located there.
a / b := a * b⁻¹
The power operation:
a ^ n = a * ··· * a
;a ^ (-n) = a⁻¹ * ··· a⁻¹
(n
times)zpow : ℤ → α → αa ^ 0 = 1
a ^ (n + 1) = a * a ^ n
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.
A linear ordered semifield is a field with a linear order respecting the operations.
Instances
The power operation:
a ^ n = a * ··· * a
;a ^ (-n) = a⁻¹ * ··· a⁻¹
(n
times)zpow : ℤ → α → αa ^ 0 = 1
a ^ (n + 1) = a * a ^ n
a ^ -(n + 1) = (a ^ (n + 1))⁻¹
- toRatCast : RatCast α
For a nonzero
a
,a⁻¹
is a right multiplicative inverse.We define the inverse of
0
to be0
.However
ratCast
is defined, propositionally it must be equal toa * b⁻¹
.Multiplication by a rational number.
qsmul : ℚ → α → αHowever
qsmul
is defined, propositionally it must be equal to multiplication byratCast
.
A linear ordered field is a field with a linear order respecting the operations.
Instances
Equations
- One or more equations did not get rendered due to their size.