def qBinomial {k : Type u_1} [Field k] (q : k) : ℕ → ℕ → k

The Gaussian (q-)binomial coefficient qBinomial q n m, defined by the recursion qBinomial q (n+1) (m+1) = q^(m+1) * qBinomial q n (m+1) + qBinomial q n m, with qBinomial q n 0 = 1 and qBinomial q 0 (m+1) = 0.

@[simp]

theorem qBinomial_zero_right {k : Type u_1} [Field k] (q : k) (n : ℕ) : qBinomial q n 0 = 1

The q-binomial coefficient with bottom index 0 equals 1.

theorem qBinomial_eq_zero_of_lt {k : Type u_1} [Field k] (q : k) (n m : ℕ) (h : n < m) : qBinomial q n m = 0

The q-binomial coefficient qBinomial q n m vanishes when n < m.

theorem qBinomial_self {k : Type u_1} [Field k] (q : k) (n : ℕ) : qBinomial q n n = 1

The q-binomial coefficient qBinomial q n n equals 1.

noncomputable def qFactorial {k : Type u_1} [Field k] (q : k) (m : ℕ) : k

The unnormalized q-factorial qFactorial q m = ∏_{i<m} (q^{i+1} - 1).

noncomputable def qFallingFact {k : Type u_1} [Field k] (q : k) (n m : ℕ) : k

The q-falling factorial qFallingFact q n m = ∏_{i<m} (q^{n-i} - 1).

theorem qFallingFact_succ_last {k : Type u_1} [Field k] (q : k) (n m : ℕ) : qFallingFact q n (m + 1) = qFallingFact q n m * (q ^ (n - m) - 1)

Recurrence: qFallingFact q n (m+1) = qFallingFact q n m * (q^{n-m} - 1).

theorem qFactorial_succ {k : Type u_1} [Field k] (q : k) (m : ℕ) : qFactorial q (m + 1) = qFactorial q m * (q ^ (m + 1) - 1)

Recurrence: qFactorial q (m+1) = qFactorial q m * (q^{m+1} - 1).

theorem qFallingFact_succ_succ {k : Type u_1} [Field k] (q : k) (n m : ℕ) : qFallingFact q (n + 1) (m + 1) = qFallingFact q n m * (q ^ (n + 1) - 1)

Reindexing recurrence: qFallingFact q (n+1) (m+1) = qFallingFact q n m * (q^{n+1} - 1).

theorem q_product_identity {k : Type u_1} [Field k] (q : k) (n m : ℕ) (hm : m ≤ n) : q ^ (m + 1) * (q ^ (n - m) - 1) + (q ^ (m + 1) - 1) = q ^ (n + 1) - 1

A q-product identity used in the recursive proof of the q-binomial formula: q^{m+1}(q^{n-m} - 1) + (q^{m+1} - 1) = q^{n+1} - 1 for m ≤ n.

theorem qBinomial_product_formula {k : Type u_1} [Field k] (q : k) (n m : ℕ) : m ≤ n → qBinomial q n m * qFactorial q m = qFallingFact q n m

Product formula for the q-binomial coefficient: qBinomial q n m * qFactorial q m = qFallingFact q n m for m ≤ n.

theorem qFallingFact_eq_zero {k : Type u_1} [Field k] (q : k) (n m : ℕ) (hqn : q ^ n = 1) (hm : 0 < m) : qFallingFact q n m = 0

The q-falling factorial qFallingFact q n m vanishes when q^n = 1 and 0 < m.

theorem qFactorial_ne_zero {k : Type u_1} [Field k] (q : k) (n m : ℕ) (hq : IsPrimitiveRoot q n) (hm : m < n) : qFactorial q m ≠ 0

If q is a primitive n-th root of unity, then qFactorial q m ≠ 0 for m < n.

theorem qBinomial_vanish {k : Type u_1} [Field k] (q : k) (n : ℕ) (_hn : 1 < n) (hq : IsPrimitiveRoot q n) (m : ℕ) (hm1 : 0 < m) (hm2 : m < n) : qBinomial q n m = 0

Vanishing of intermediate q-binomial coefficients at a primitive root of unity: if q is a primitive n-th root of unity (n > 1) then qBinomial q n m = 0 for 0 < m < n.

theorem q_comm_pow_right {k : Type u_1} [Field k] {A : Type u_2} [Ring A] [Algebra k A] (q : k) (a b : A) (hcomm : b * a = (algebraMap k A) q * (a * b)) (m : ℕ) : b ^ m * a = (algebraMap k A) (q ^ m) * (a * b ^ m)

If ba = q · ab then b^m · a = q^m · (a · b^m).

theorem term_mul_add {k : Type u_1} [Field k] {A : Type u_2} [Ring A] [Algebra k A] (q : k) (a b : A) (hcomm : b * a = (algebraMap k A) q * (a * b)) (c : k) (p m : ℕ) : (algebraMap k A) c * (a ^ p * b ^ m) * (a + b) = (algebraMap k A) (c * q ^ m) * (a ^ (p + 1) * b ^ m) + (algebraMap k A) c * (a ^ p * b ^ (m + 1))

Auxiliary identity used in the proof of the q-binomial expansion: multiplying c · a^p b^m by (a + b) produces the expected two-term sum involving a factor of q^m.

theorem q_binomial_expansion {k : Type u_1} [Field k] {A : Type u_2} [Ring A] [Algebra k A] (q : k) (a b : A) (hcomm : b * a = (algebraMap k A) q * (a * b)) (n : ℕ) : (a + b) ^ n = ∑ m ∈ Finset.range (n + 1), (algebraMap k A) (qBinomial q n m) * (a ^ (n - m) * b ^ m)

q-Binomial expansion: if ba = q · ab in A then (a+b)^n = ∑_{m=0}^{n} (q-binomial coefficient) · a^{n-m} b^m.

theorem q_comm_power {k : Type u_1} [Field k] {A : Type u_2} [Ring A] [Algebra k A] (q : k) (n : ℕ) (hn : 1 < n) (hq : IsPrimitiveRoot q n) (a b : A) (hcomm : b * a = (algebraMap k A) q * (a * b)) : (a + b) ^ n = a ^ n + b ^ n

Frobenius-type identity at a primitive root of unity: if q is a primitive n-th root of unity (n > 1) and ba = q · ab in A, then (a + b)^n = a^n + b^n.