Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-18 16:41 80071d45

View on Github →

refactor(algebra/floor): Add ceil as a field of floor_ring (#9591) This allows more control on definitional equality.

Estimated changes

modified def int.ceil
modified theorem int.ceil_eq_iff
modified theorem int.ceil_le
modified theorem int.ceil_mono
modified theorem int.ceil_neg
modified theorem int.ceil_nonneg
modified theorem int.ceil_pos
modified theorem int.floor_eq_iff
modified theorem int.floor_le
modified theorem int.floor_lt
modified theorem int.floor_mono
modified theorem int.floor_neg
modified theorem int.floor_nonneg
added theorem int.floor_ring_ceil_eq
added theorem int.gc_ceil_coe
added theorem int.gc_coe_floor
modified theorem int.le_ceil
modified theorem int.le_floor
modified theorem int.lt_ceil
modified theorem int.preimage_Ici
modified theorem int.preimage_Iic
modified theorem int.preimage_Iio
modified theorem int.preimage_Ioi
modified theorem nat.ceil_add_nat
modified theorem nat.ceil_add_one
modified theorem nat.ceil_lt_add_one
modified theorem nat.floor_add_one
modified theorem nat.le_of_ceil_le
modified theorem nat.lt_of_ceil_lt