Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-07 18:31 e871be25

View on Github →

feat(data/real/nnreal): floor_semiring instance (#12495) Zulip thread

Estimated changes

Modified src/algebra/order/floor.lean

Modified src/algebra/order/nonneg.lean

added theorem nonneg.nat_ceil_coe

added theorem nonneg.nat_floor_coe

Modified src/data/real/nnreal.lean