Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-26 15:40 d1cbb8f0

View on Github →

fix(algebra/group): add every transport theorem from main Lean repository

Estimated changes

deleted def finset.card
deleted theorem finset.card_empty
deleted theorem finset.card_erase_of_mem
deleted theorem finset.card_insert_le
deleted theorem finset.card_insert_of_mem
deleted theorem finset.card_upto
deleted def finset.empty
deleted theorem finset.empty_inter
deleted theorem finset.empty_subset
deleted theorem finset.empty_union
deleted theorem finset.eq_of_singleton_eq
deleted def finset.erase
deleted theorem finset.erase_empty
deleted theorem finset.erase_insert
deleted theorem finset.erase_subset
deleted theorem finset.erase_subset_erase
deleted theorem finset.ext
deleted theorem finset.insert.comm
deleted def finset.insert
deleted theorem finset.insert_eq
deleted theorem finset.insert_eq_of_mem
deleted theorem finset.insert_erase
deleted theorem finset.insert_union
deleted def finset.inter
deleted theorem finset.inter_assoc
deleted theorem finset.inter_comm
deleted theorem finset.inter_distrib_left
deleted theorem finset.inter_empty
deleted theorem finset.inter_left_comm
deleted theorem finset.inter_right_comm
deleted theorem finset.inter_self
deleted theorem finset.lt_of_mem_upto
deleted def finset.mem
deleted theorem finset.mem_empty_iff
deleted theorem finset.mem_erase_iff
deleted theorem finset.mem_insert
deleted theorem finset.mem_insert_iff
deleted theorem finset.mem_insert_of_mem
deleted theorem finset.mem_inter
deleted theorem finset.mem_inter_iff
deleted theorem finset.mem_list_of_mem
deleted theorem finset.mem_of_mem_erase
deleted theorem finset.mem_of_mem_list
deleted theorem finset.mem_singleton
deleted theorem finset.mem_singleton_iff
deleted theorem finset.mem_to_finset
deleted theorem finset.mem_union_iff
deleted theorem finset.mem_union_l
deleted theorem finset.mem_union_left
deleted theorem finset.mem_union_r
deleted theorem finset.mem_union_right
deleted theorem finset.mem_upto_iff
deleted theorem finset.mem_upto_of_lt
deleted theorem finset.ne_of_mem_erase
deleted theorem finset.not_mem_empty
deleted theorem finset.not_mem_erase
deleted theorem finset.pair_eq_singleton
deleted theorem finset.singleton_ne_empty
deleted theorem finset.subset.antisymm
deleted theorem finset.subset.refl
deleted theorem finset.subset.trans
deleted def finset.subset
deleted def finset.subset_aux
deleted theorem finset.subset_empty_iff
deleted theorem finset.subset_insert
deleted theorem finset.subset_insert_iff
deleted theorem finset.subset_of_forall
deleted def finset.to_finset
deleted def finset.union
deleted theorem finset.union_assoc
deleted theorem finset.union_comm
deleted theorem finset.union_distrib_left
deleted theorem finset.union_empty
deleted theorem finset.union_left_comm
deleted theorem finset.union_right_comm
deleted theorem finset.union_self
deleted def finset.upto
deleted theorem finset.upto_succ
deleted theorem finset.upto_zero
deleted def finset
deleted def nodup_list
deleted def to_nodup_list