Multiset coefficients
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-08-07.
Last modified on 2024-10-09.
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 other
words, it counts the number of
connected componets of the type
Σ (A : Fin n → 𝔽), ║ Fin k ≃ Σ (i : Fin n), A i ║.
The first few numbers are
| n\k | 0 | 1 | 2 | 3 | 4 | 5 |
|---|---|---|---|---|---|---|
| 0 | 1 | 0 | 0 | 0 | 0 | 0 |
| 1 | 1 | 1 | 1 | 1 | 1 | 1 |
| 2 | 1 | 2 | 3 | 4 | 5 | 6 |
| 3 | 1 | 3 | 6 | 10 | 15 | 21 |
| 4 | 1 | 4 | 10 | 20 | 35 | 56 |
| 5 | 1 | 5 | 15 | 35 | 70 | 126 |
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
- 2024-10-09. Fredrik Bakke. Idea text
set-theory(#1189). - 2023-05-16. Fredrik Bakke. Swap from
mdtotextcode blocks (#622). - 2023-05-13. Fredrik Bakke. Refactor to use infix binary operators for arithmetic (#620).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>tags and markdown syntax (#490).