Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-06 12:41 f4207aa2

View on Github →

feat(data/*): lemmas about lists and finsets (#4457) A part of #4316

Estimated changes

modified theorem finset.prod_mk
added theorem fin.univ_def
added theorem finset.univ_eq_empty
modified theorem finset.univ_nonempty
added theorem fin.prod_of_fn
added theorem fin.prod_univ_def
added theorem list.attach_eq_nil
added theorem list.pmap_eq_nil
added theorem list.prod_update_nth
added theorem list.nodup.map_update
added theorem list.of_fn_const
modified theorem list.of_fn_succ
modified theorem list.of_fn_zero
added theorem list.fin_range_eq_nil
added theorem list.fin_range_zero
added theorem list.of_fn_eq_map
added theorem list.of_fn_id
added theorem list.range'_eq_nil
added theorem list.range_eq_nil