Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-10 16:03 2e8ef55f

View on Github →

feat(algebra/floor): nat_floor (#7855) introduce nat_floor Related Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/nat_floor

Estimated changes

added theorem le_nat_floor_iff
added theorem le_nat_floor_of_le
modified theorem lt_nat_ceil
added theorem lt_nat_floor_add_one
added theorem lt_of_lt_nat_floor
modified def nat_ceil
modified theorem nat_ceil_le
added def nat_floor
added theorem nat_floor_add_nat
added theorem nat_floor_coe
added theorem nat_floor_eq_zero_iff
added theorem nat_floor_le
added theorem nat_floor_lt_iff
added theorem nat_floor_mono
added theorem nat_floor_of_nonpos
added theorem nat_floor_zero
added theorem pos_of_nat_floor_pos
added theorem int.to_nat_add_nat
deleted theorem int.to_nat_add_one
added theorem int.to_nat_of_nonpos
deleted theorem int.to_nat_zero_of_neg