Mathlib Changelog
v3
Changelog
About
Github
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
Modified
algebra/group.lean
Deleted
data/finset/basic.lean
deleted
def
finset.card
deleted
theorem
finset.card_empty
deleted
theorem
finset.card_erase_of_mem
deleted
theorem
finset.card_erase_of_not_mem
deleted
theorem
finset.card_insert_le
deleted
theorem
finset.card_insert_of_mem
deleted
theorem
finset.card_insert_of_not_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_empty_of_card_eq_zero
deleted
theorem
finset.eq_empty_of_forall_not_mem
deleted
theorem
finset.eq_empty_of_subset_empty
deleted
theorem
finset.eq_of_mem_singleton
deleted
theorem
finset.eq_of_singleton_eq
deleted
theorem
finset.eq_of_subset_of_subset
deleted
theorem
finset.eq_or_mem_of_mem_insert
deleted
def
finset.erase
deleted
theorem
finset.erase_empty
deleted
theorem
finset.erase_eq_of_not_mem
deleted
theorem
finset.erase_insert
deleted
theorem
finset.erase_insert_subset
deleted
theorem
finset.erase_subset
deleted
theorem
finset.erase_subset_erase
deleted
theorem
finset.erase_subset_of_subset_insert
deleted
theorem
finset.exists_mem_empty_iff
deleted
theorem
finset.exists_mem_insert_iff
deleted
theorem
finset.exists_mem_of_ne_empty
deleted
theorem
finset.ext
deleted
theorem
finset.forall_mem_empty_iff
deleted
theorem
finset.forall_mem_insert_iff
deleted
theorem
finset.forall_of_forall_insert
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_erase_subset
deleted
theorem
finset.insert_subset_insert
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_distrib_right
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_erase_of_ne_of_mem
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_insert_of_ne
deleted
theorem
finset.mem_of_mem_inter_left
deleted
theorem
finset.mem_of_mem_inter_right
deleted
theorem
finset.mem_of_mem_list
deleted
theorem
finset.mem_of_subset_of_mem
deleted
theorem
finset.mem_or_mem_of_mem_union
deleted
theorem
finset.mem_singleton
deleted
theorem
finset.mem_singleton_iff
deleted
theorem
finset.mem_singleton_of_eq
deleted
theorem
finset.mem_to_finset
deleted
theorem
finset.mem_to_finset_of_nodup
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.mem_upto_succ_of_mem_upto
deleted
theorem
finset.ne_empty_of_card_eq_succ
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.perm_insert_cons_of_not_mem
deleted
theorem
finset.singleton_inter_of_mem
deleted
theorem
finset.singleton_inter_of_not_mem
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_insert_of_erase_subset
deleted
theorem
finset.subset_of_forall
deleted
def
finset.to_finset
deleted
theorem
finset.to_finset_eq_of_nodup
deleted
def
finset.to_finset_of_nodup
deleted
def
finset.union
deleted
theorem
finset.union_assoc
deleted
theorem
finset.union_comm
deleted
theorem
finset.union_distrib_left
deleted
theorem
finset.union_distrib_right
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
deleted
def
to_nodup_list_of_nodup
Modified
data/list/set.lean
deleted
theorem
list.length_erase_of_not_mem
Modified
topology/real.lean