mathlib documentation


Canonically ordered semifields #

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

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]