Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-06 11:48 43e01caf

View on Github →

split(algebra/order/nonneg): Separate ring and field instances (#17348) Split algebra.order.nonneg into:

algebra.order.nonneg.ring for ring instances
algebra.order.nonneg.field for field and archimedean instances

Estimated changes

Created src/algebra/order/nonneg/field.lean

added theorem nonneg.inv_mk

added theorem nonneg.mk_div_mk

added theorem nonneg.mk_zpow

added theorem nonneg.nat_ceil_coe

added theorem nonneg.nat_floor_coe

Renamed src/algebra/order/nonneg.lean to src/algebra/order/nonneg/ring.lean

deleted theorem nonneg.inv_mk

deleted theorem nonneg.mk_div_mk

added theorem nonneg.mk_nat_cast

deleted theorem nonneg.mk_zpow

deleted theorem nonneg.nat_ceil_coe

deleted theorem nonneg.nat_floor_coe

Modified src/data/rat/nnrat.lean

Modified src/data/real/nnreal.lean