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