Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-24 00:43 c374a3b9

View on Github →

feat(data/nat/nth): add nth function (#10707) Split off from #9457, introduces nth and proves theorems about it.

Estimated changes

added theorem nat.count_injective
added theorem nat.count_le_card
added theorem nat.count_lt_card
modified theorem nat.count_monotone
added theorem nat.count_strict_mono
added theorem nat.count_nth_gc
added theorem nat.count_nth_zero
added theorem nat.le_nth_of_count_le
added theorem nat.nth_count
added theorem nat.nth_count_eq_Inf
added theorem nat.nth_count_le
added theorem nat.nth_lt_of_lt_count
added theorem nat.nth_mono_of_finite
added theorem nat.nth_monotone
added theorem nat.nth_set_card
added theorem nat.nth_set_card_aux
added theorem nat.nth_strict_mono
added theorem nat.nth_zero
added theorem nat.nth_zero_of_exists
added theorem nat.nth_zero_of_zero