Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-11 10:34 9925a115

View on Github →

chore(data/list/range): split & reduce imports (#17887) This PR splits most of the lemmas about list.fin_range into a new file. list.fin_range is much less useful than list.range, but we need to import data.list.of_fn for list.fin_range, and then data.list.of_fn imports data.fin.tuple.basic and data.fin.tuple.basic imports many things.

Estimated changes

added theorem list.map_coe_fin_range
added theorem list.map_nth_le
added theorem list.nodup_of_fn
added theorem list.of_fn_eq_map
added theorem list.of_fn_eq_pmap
added theorem list.of_fn_id
deleted theorem list.map_coe_fin_range
deleted theorem list.map_nth_le
deleted theorem list.nodup_of_fn
deleted theorem list.of_fn_eq_map
deleted theorem list.of_fn_eq_pmap
deleted theorem list.of_fn_id