Count a fixed block total by a binomial coefficient
ProvedOAI.PiExponent.LiteralAnalytic.blockFiber_cardnumber-theoryopenai-pi-exponent-017
The number of assignments of total n to m slots is the weak-composition coefficient. This includes m = 0: the fiber has one element for n = 0 and is empty for positive n, matching the natural-number binomial expression.
Preamble
import Mathlib.Tactic open scoped BigOperators
Formal statement
theorem OAI.PiExponent.LiteralAnalytic.blockFiber_card
(m n : ℕ) :
Fintype.card
{g : Fin m → Fin (n + 1) //
Finset.univ.sum (fun j => (g j).val) = n} =
Nat.choose (n + m - 1) n := by sorrySource