mathlib
1c2d71f1 - feat(algebra/order/field): Canonically linear ordered semifields (#15677)

Commit
3 years ago
feat(algebra/order/field): Canonically linear ordered semifields (#15677) Define `canonically_linear_ordered_semifield`. The target is `nnreal` and the future `nnrat`.
Author
Parents
Loading