Commit 2022-08-27 21:53 1c2d71f1

View on Github →

feat(algebra/order/field): Canonically linear ordered semifields (#15677) Define canonically_linear_ordered_semifield. The target is nnreal and the future nnrat.

Estimated changes

Modified src/algebra/order/field.lean

added theorem tsub_div

Modified src/algebra/order/field_defs.lean

Modified src/algebra/order/nonneg.lean

modified theorem nonneg.inv_mk

modified theorem nonneg.mk_div_mk

added theorem nonneg.mk_zpow