Documentation

Mathlib.Algebra.Order.Field.Defs

Linear ordered (semi)fields #

A linear ordered (semi)field is a (semi)field equipped with a linear order such that

Main Definitions #

@[deprecated "Use `[Semifield K] [LinearOrder K] [IsStrictOrderedRing K]` instead." (since := "2025-04-10")]

A linear ordered semifield is a field with a linear order respecting the operations.

Instances For
    @[deprecated "Use `[Field K] [LinearOrder K] [IsStrictOrderedRing K]` instead." (since := "2025-04-10")]
    structure LinearOrderedField (K : Type u_1) extends LinearOrderedCommRing K, Field K :
    Type u_1

    A linear ordered field is a field with a linear order respecting the operations.

    Instances For