Pair-content to tuple equivalence

The set of pair-contents with prescribed row and column margins bijects with the set of row-wise multisets with matching column margins.

theorem RS.pair_tuple_card {n k : ℕ} (α β : Fin k → ℕ) (hα : ∑ a : Fin k, α a = n) : Fintype.card { s : Sym (Fin k × Fin k) n // (∀ (a : Fin k), ∑ b : Fin k, Multiset.count (a, b) ↑s = α a) ∧ ∀ (b : Fin k), ∑ a : Fin k, Multiset.count (a, b) ↑s = β b } = Fintype.card { W : (a : Fin k) → Sym (Fin k) (α a) // ∀ (b : Fin k), ∑ a : Fin k, Multiset.count b ↑(W a) = β b }

Pair-contents with prescribed margins biject with row-wise multisets matching the column margins.