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.
@[deprecated "Use `[Semifield K] [LinearOrder K] [IsStrictOrderedRing K]` instead." (since := "2025-04-10")]
structure
LinearOrderedSemifield
(K : Type u_1)
extends LinearOrderedCommSemiring K, Semifield K :
Type u_1
A linear ordered semifield is a field with a linear order respecting the operations.
- add : K → K → K
- zero : K
- mul : K → K → K
- one : K
- min : K → K → K
- max : K → K → K
- inv : K → K
- div : K → K → K
Instances For
@[deprecated "Use `[Field K] [LinearOrder K] [IsStrictOrderedRing K]` instead." (since := "2025-04-10")]
A linear ordered field is a field with a linear order respecting the operations.
- add : K → K → K
- zero : K
- mul : K → K → K
- one : K
- neg : K → K
- sub : K → K → K
- min : K → K → K
- max : K → K → K
- inv : K → K
- div : K → K → K