Multiset coefficients

Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.

Created on 2022-08-07.
Last modified on 2023-05-16.

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))

Recent changes