mathlib documentation

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 #

Implementation details #

For olean caching reasons, this file is separate to the main file, algebra.order.field. The lemmata are instead located there.

@[class]
structure linear_ordered_semifield (α : Type u_2) :
Type u_2

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

Instances of this typeclass
Instances of other typeclasses for linear_ordered_semifield
  • linear_ordered_semifield.has_sizeof_inst
@[instance]
@[instance]
def linear_ordered_field.to_field (α : Type u_2) [self : linear_ordered_field α] :
@[class]
structure linear_ordered_field (α : Type u_2) :
Type u_2

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

Instances of this typeclass
Instances of other typeclasses for linear_ordered_field
  • linear_ordered_field.has_sizeof_inst
@[class]
structure canonically_linear_ordered_semifield (α : Type u_2) :
Type u_2

A canonically linear ordered field is a linear ordered field in which a ≤ b iff there exists c with b = a + c.

Instances of this typeclass
Instances of other typeclasses for canonically_linear_ordered_semifield
  • canonically_linear_ordered_semifield.has_sizeof_inst
@[protected, instance]
Equations
@[protected, instance]
Equations