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
- 2023-05-16. Fredrik Bakke. Swap from
md
totext
code 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). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).