Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-26 13:03 67a2f398

View on Github →

refactor(data/finset): add type class instances

Estimated changes

Modified data/finset/basic.lean

modified theorem finset.eq_of_mem_singleton

modified theorem finset.eq_of_singleton_eq

deleted theorem finset.exists_mem_empty_eq

modified theorem finset.exists_mem_empty_iff

deleted theorem finset.exists_mem_insert_eq

modified theorem finset.exists_mem_insert_iff

deleted theorem finset.forall_mem_empty_eq

modified theorem finset.forall_mem_empty_iff

deleted theorem finset.forall_mem_insert_eq

modified theorem finset.forall_mem_insert_iff

modified theorem finset.forall_of_forall_insert

modified theorem finset.insert_eq

deleted theorem finset.mem_empty_eq

deleted theorem finset.mem_erase_eq

deleted theorem finset.mem_insert_eq

deleted theorem finset.mem_inter_eq

modified theorem finset.mem_list_of_mem

modified theorem finset.mem_of_mem_list

modified theorem finset.mem_singleton

modified theorem finset.mem_singleton_iff

modified theorem finset.mem_singleton_of_eq

deleted theorem finset.mem_union_eq

deleted theorem finset.mem_upto_eq

modified theorem finset.pair_eq_singleton

modified theorem finset.singleton_ne_empty

modified theorem finset.upto_succ