Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2019-04-16 18:10
22948763
View on Github →
feat(data/finset): powerset_len (subsets of a given size) (
#899
)
feat(data/finset): powerset_len (subsets of a given size)
fix build
Estimated changes
Modified
src/algebra/char_p.lean
Modified
src/data/complex/exponential.lean
Modified
src/data/finset.lean
added
theorem
finset.card_powerset_len
added
theorem
finset.mem_powerset_len
added
def
finset.powerset_len
added
theorem
finset.powerset_len_mono
Modified
src/data/list/basic.lean
added
theorem
list.append_sublist_append
added
theorem
list.length_of_sublists_len
added
theorem
list.length_sublists_len
added
theorem
list.mem_sublists_len
added
theorem
list.mem_sublists_len_self
added
theorem
list.nodup_sublists_len
added
def
list.sublists_len
added
def
list.sublists_len_aux
added
theorem
list.sublists_len_aux_append
added
theorem
list.sublists_len_aux_eq
added
theorem
list.sublists_len_aux_zero
added
theorem
list.sublists_len_sublist_of_sublist
added
theorem
list.sublists_len_sublist_sublists'
added
theorem
list.sublists_len_succ_cons
added
theorem
list.sublists_len_succ_nil
added
theorem
list.sublists_len_zero
Modified
src/data/multiset.lean
added
theorem
multiset.card_powerset_len
added
theorem
multiset.mem_powerset_len
added
theorem
multiset.mem_powerset_len_aux
added
theorem
multiset.nodup_powerset_len
added
def
multiset.powerset_len
added
def
multiset.powerset_len_aux
added
theorem
multiset.powerset_len_aux_cons
added
theorem
multiset.powerset_len_aux_eq_map_coe
added
theorem
multiset.powerset_len_aux_nil
added
theorem
multiset.powerset_len_aux_perm
added
theorem
multiset.powerset_len_aux_zero
added
theorem
multiset.powerset_len_coe'
added
theorem
multiset.powerset_len_coe
added
theorem
multiset.powerset_len_cons
added
theorem
multiset.powerset_len_le_powerset
added
theorem
multiset.powerset_len_mono
added
theorem
multiset.powerset_len_zero_left
added
theorem
multiset.powerset_len_zero_right
Modified
src/data/nat/basic.lean
added
def
nat.choose
added
theorem
nat.choose_eq_fact_div_fact
added
theorem
nat.choose_eq_zero_of_lt
added
theorem
nat.choose_mul_fact_mul_fact
added
theorem
nat.choose_one_right
added
theorem
nat.choose_pos
added
theorem
nat.choose_self
added
theorem
nat.choose_succ_self
added
theorem
nat.choose_succ_succ
added
theorem
nat.choose_zero_right
added
theorem
nat.choose_zero_succ
added
theorem
nat.fact_mul_fact_dvd_fact
added
theorem
nat.succ_mul_choose_eq
Modified
src/data/nat/choose.lean
deleted
def
choose
deleted
theorem
choose_eq_fact_div_fact
deleted
theorem
choose_eq_zero_of_lt
deleted
theorem
choose_mul_fact_mul_fact
deleted
theorem
choose_one_right
deleted
theorem
choose_pos
deleted
theorem
choose_self
deleted
theorem
choose_succ_self
deleted
theorem
choose_succ_succ
deleted
theorem
choose_zero_right
deleted
theorem
choose_zero_succ
deleted
theorem
fact_mul_fact_dvd_fact
deleted
theorem
succ_mul_choose_eq
Modified
src/ring_theory/ideal_operations.lean