Commit 2023-06-21 10:32 615e31fb

View on Github →

feat: port Data.Nat.Nth (#2297)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Nth.lean

added theorem Nat.count_le_iff_le_nth

added theorem Nat.count_nth

added theorem Nat.count_nth_of_infinite

added theorem Nat.count_nth_of_lt_card_finite

added theorem Nat.count_nth_succ

added theorem Nat.count_nth_zero

added theorem Nat.exists_lt_card_finite_nth_eq

added theorem Nat.exists_lt_card_nth_eq

added theorem Nat.filter_range_nth_eq_insert

added theorem Nat.filter_range_nth_eq_insert_of_finite

added theorem Nat.filter_range_nth_eq_insert_of_infinite

added theorem Nat.filter_range_nth_subset_insert

added theorem Nat.gc_count_nth

added theorem Nat.image_nth_Iio_card

added theorem Nat.isLeast_nth

added theorem Nat.isLeast_nth_of_infinite

added theorem Nat.isLeast_nth_of_lt_card

added theorem Nat.le_nth

added theorem Nat.le_nth_count'

added theorem Nat.le_nth_count

added theorem Nat.le_nth_of_count_le

added theorem Nat.le_nth_of_lt_nth_succ

added theorem Nat.le_of_nth_le_nth_of_lt_card

added theorem Nat.lt_nth_iff_count_lt

added theorem Nat.lt_of_nth_lt_nth_of_lt_card

added theorem Nat.nth_apply_eq_orderIsoOfNat

added theorem Nat.nth_count

added theorem Nat.nth_count_eq_sInf

added theorem Nat.nth_eq_getD_sort

added theorem Nat.nth_eq_orderEmbOfFin

added theorem Nat.nth_eq_orderIsoOfNat

added theorem Nat.nth_eq_sInf

added theorem Nat.nth_eq_zero

added theorem Nat.nth_eq_zero_mono

added theorem Nat.nth_injOn

added theorem Nat.nth_injective

added theorem Nat.nth_le_nth'

added theorem Nat.nth_le_nth

added theorem Nat.nth_le_nth_of_lt_card

added theorem Nat.nth_lt_nth'

added theorem Nat.nth_lt_nth

added theorem Nat.nth_lt_nth_of_lt_card

added theorem Nat.nth_lt_of_lt_count

added theorem Nat.nth_mem

added theorem Nat.nth_mem_of_infinite

added theorem Nat.nth_mem_of_lt_card

added theorem Nat.nth_monotone

added theorem Nat.nth_of_card_le

added theorem Nat.nth_strictMono

added theorem Nat.nth_strictMonoOn

added theorem Nat.nth_zero

added theorem Nat.nth_zero_of_exists

added theorem Nat.nth_zero_of_zero

added theorem Nat.range_nth_of_finite

added theorem Nat.range_nth_of_infinite

added theorem Nat.range_nth_subset

added theorem Nat.subset_range_nth