Commit 2024-04-05 20:49 7239f2e9

View on Github →

chore(Data/List/Card): Delete (#11846) As prophecised by the module doc, this file has been made fully redundant by the advent of Finset

Estimated changes

deleted def List.card
deleted theorem List.card_append_disjoint
deleted theorem List.card_cons_of_mem
deleted theorem List.card_cons_of_not_mem
deleted theorem List.card_eq_of_equiv
deleted theorem List.card_insert_of_mem
deleted theorem List.card_le_card_cons
deleted theorem List.card_map_le
deleted theorem List.card_nil
deleted theorem List.card_remove_of_mem
deleted theorem List.card_subset_le
deleted theorem List.card_union_disjoint
deleted def List.inj_on
deleted theorem List.inj_on_of_subset
deleted theorem List.insert_equiv_cons
deleted theorem List.mem_of_mem_remove
deleted theorem List.mem_remove_iff
deleted def List.remove
deleted theorem List.remove_eq_of_not_mem
deleted theorem List.union_equiv_append