Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-22 15:58 03ba4ccf

View on Github →

feat(algebra/floor): Floor semirings (#9592) A floor semiring is a semiring equipped with a floor and a ceil function.

Estimated changes

added theorem floor_semiring_unique
added theorem int.ceil_to_nat
added theorem int.floor_nonpos
added theorem int.floor_to_nat
modified def nat.ceil
modified theorem nat.ceil_eq_zero
modified theorem nat.ceil_le
modified theorem nat.ceil_mono
modified def nat.floor
added theorem nat.floor_eq_iff
added theorem nat.floor_eq_on_Ico'
added theorem nat.floor_eq_on_Ico
added theorem nat.floor_eq_zero
deleted theorem nat.floor_eq_zero_iff
modified theorem nat.floor_le
added theorem nat.floor_lt'
added theorem nat.floor_lt
deleted theorem nat.floor_lt_iff
modified theorem nat.floor_mono
added theorem nat.floor_one
added theorem nat.gc_ceil_coe
added theorem nat.le_floor
added theorem nat.le_floor_iff'
modified theorem nat.le_floor_iff
deleted theorem nat.le_floor_of_le
modified theorem nat.lt_ceil
modified theorem nat.lt_floor_add_one
added theorem nat.lt_of_floor_lt
added theorem nat.lt_succ_floor
modified theorem nat.sub_one_lt_floor
added theorem int.le_to_nat_iff