Finite q-binomial theorem

This file proves the finite q-binomial theorem: $$\prod_{k=0}^{n-1}(1 + z q^k) = \sum_{k=0}^{n} q^{\binom{k}{2}} \binom{n}{k}_q z^k.$$

Main results

• QSeries.prod_one_add_mul_pow_eq_sum_qBinom — the finite q-binomial theorem.

theorem QSeries.prod_one_add_mul_pow_eq_sum_qBinom {R : Type u_1} [CommRing R] (q z : R) (n : ℕ) : ∏ k ∈ Finset.range n, (1 + z * q ^ k) = ∑ k ∈ Finset.range (n + 1), q ^ k.choose 2 * qBinom n k q * z ^ k

Finite q-binomial theorem. $$\prod_{k=0}^{n-1}(1 + z q^k) = \sum_{k=0}^{n} q^{\binom{k}{2}} \binom{n}{k}_q z^k.$$