doc-next-gen

Mathlib.Algebra.Order.Field.Defs

Module docstring

{"# 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. "}
LinearOrderedSemifield structure
(K : Type*) extends LinearOrderedCommSemiring K, Semifield K
Full source 
/-- A linear ordered semifield is a field with a linear order respecting the operations. -/
@[deprecated "Use `[Semifield K] [LinearOrder K] [IsStrictOrderedRing K]` instead."
  (since := "2025-04-10")]
structure LinearOrderedSemifield (K : Type*) extends LinearOrderedCommSemiring K, Semifield K
Linear Ordered Semifield
Informal description
A linear ordered semifield is a semifield $K$ equipped with a linear order such that: 1. Addition respects the order: for all $a, b, c \in K$, if $a \leq b$ then $c + a \leq c + b$. 2. Multiplication of positive elements is positive: for all $a, b \in K$, if $0 < a$ and $0 < b$ then $0 < a \cdot b$. 3. The element $1$ is positive: $0 < 1$.
LinearOrderedField structure
(K : Type*) extends LinearOrderedCommRing K, Field K
Full source 
/-- A linear ordered field is a field with a linear order respecting the operations. -/
@[deprecated "Use `[Field K] [LinearOrder K] [IsStrictOrderedRing K]` instead."
  (since := "2025-04-10")]
structure LinearOrderedField (K : Type*) extends LinearOrderedCommRing K, Field K
Linear Ordered Field
Informal description
A linear ordered field is a field \( K \) equipped with a linear order that is compatible with the field operations: 1. Addition respects the order: for all \( a, b, c \in K \), if \( a \leq b \), then \( c + a \leq c + b \). 2. Multiplication of positive elements is positive: for all \( a, b \in K \), if \( 0 < a \) and \( 0 < b \), then \( 0 < a \cdot b \). 3. The multiplicative identity is positive: \( 0 < 1 \).