mathlib3 documentation

algebra.order.field.defs

Linear ordered (semi)fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.basic. 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]
@[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
@[protected, instance]
Equations