Commit 2023-01-10 22:47 cbea84f3

View on Github →

feat: port Mathlib.Data.List.Range (#1463)

Estimated changes

Modified Mathlib/Data/Fintype/Basic.lean

Modified Mathlib/Data/List/Range.lean

added theorem List.chain'_range_succ

added theorem List.chain_range_succ

modified theorem List.chain_succ_range'

added theorem List.enum_eq_zip_range

added theorem List.enum_from_eq_zip_range'

added theorem List.enum_from_map_fst

added theorem List.enum_map_fst

modified def List.finRange

added theorem List.finRange_eq_nil

added theorem List.finRange_zero

deleted theorem List.fin_range_zero

added theorem List.get?_range'

added theorem List.get_finRange

added theorem List.get_range'

added theorem List.get_range

added theorem List.iota_eq_reverse_range'

added theorem List.length_finRange

added theorem List.length_iota

added theorem List.length_range'

added theorem List.length_range

added theorem List.map_add_range'

added theorem List.map_sub_range'

added theorem List.mem_finRange

deleted theorem List.mem_fin_range

added theorem List.mem_iota

added theorem List.nodup_finRange

deleted theorem List.nodup_fin_range

added theorem List.nodup_iota

modified theorem List.nodup_range

added theorem List.not_mem_range_self

added theorem List.nthLe_finRange

added theorem List.nthLe_range

added theorem List.nth_le_range'

added theorem List.nth_range

added theorem List.pairwise_gt_iota

added theorem List.pairwise_le_range

added theorem List.pairwise_lt_range

added theorem List.prod_range_succ'

added theorem List.prod_range_succ

added theorem List.range'_append

added theorem List.range'_concat

added theorem List.range'_eq_map_range

added theorem List.range'_eq_nil

added theorem List.range'_sublist_right

added theorem List.range'_subset_right

added theorem List.range_add

added theorem List.range_eq_nil

added theorem List.range_sublist

added theorem List.range_subset

added theorem List.range_succ

added theorem List.range_succ_eq_map

added theorem List.range_zero

added theorem List.reverse_range'

added theorem List.self_mem_range_succ

added theorem List.unzip_enum_eq_prod

added theorem List.unzip_enum_from_eq_prod