Commit 2023-04-07 13:27 520ecd2c

View on Github →

feat: port Data.Nat.Choose.Multinomial (#2361)

depends on: #2168

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Choose/Multinomial.lean

added theorem Finset.sum_pow

added theorem Finset.sum_pow_of_commute

added def Finsupp.multinomial

added theorem Finsupp.multinomial_eq

added theorem Finsupp.multinomial_update

added theorem Multiset.multinomial_filter_ne

added theorem Nat.binomial_eq

added theorem Nat.binomial_eq_choose

added theorem Nat.binomial_one

added theorem Nat.binomial_spec

added theorem Nat.binomial_succ_succ

added def Nat.multinomial

added theorem Nat.multinomial_congr

added theorem Nat.multinomial_insert

added theorem Nat.multinomial_insert_one

added theorem Nat.multinomial_nil

added theorem Nat.multinomial_pos

added theorem Nat.multinomial_singleton

added theorem Nat.multinomial_spec

added theorem Nat.multinomial_univ_three

added theorem Nat.multinomial_univ_two

added theorem Nat.succ_mul_binomial