This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
Multiset coefficients
module elementary-number-theory.multiset-coefficients where
Imports
open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers
Idea
The multiset coefficients count the number of multisets of size k of elements
of a set of size n. In oter words, it counts the number of connected componets
of the type
Σ (A : Fin n → 𝔽), ∥ Fin k ≃ Σ (i : Fin n), A i ∥.
Definition
multiset-coefficient : ℕ → ℕ → ℕ multiset-coefficient zero-ℕ zero-ℕ = 1 multiset-coefficient zero-ℕ (succ-ℕ k) = 0 multiset-coefficient (succ-ℕ n) zero-ℕ = 1 multiset-coefficient (succ-ℕ n) (succ-ℕ k) = (multiset-coefficient (succ-ℕ n) k) +ℕ (multiset-coefficient n (succ-ℕ k))