Finite products and sums in a field

Factoring the leading power out of a product of q ^ k - 1

For q ≠ 0 in a field, ∏ i ∈ s, (q ^ f i - 1) = q ^ (∑ i ∈ s, f i) * ∏ i ∈ s, (1 - (q ^ f i)⁻¹). This is how the orders of the finite classical groups, which are products of factors q ^ k - 1, become the normalized values ∏ (1 - q^{-k}) of local densities.

Main results

• Finset.prod_pow_sub_one: factoring q ^ (∑ i ∈ s, f i) out of ∏ i ∈ s, (q ^ f i - 1).
• Finset.sum_range_add_mul_add_div_two: the increments of a quadratic along a uniform grid sum to the increment of the quadratic from 0 to the end of the grid.

theorem Finset.prod_pow_sub_one {K : Type u_1} {ι : Type u_2} [Field K] {q : K} (hq : q ≠ 0) (s : Finset ι) (f : ι → ℕ) : ∏ i ∈ s, (q ^ f i - 1) = (q ^ ∑ i ∈ s, f i) * ∏ i ∈ s, (1 - (q ^ f i)⁻¹)

Factoring the leading power out of a product of q ^ k - 1. For q ≠ 0 in a field, ∏ i ∈ s, (q ^ f i - 1) = q ^ (∑ i ∈ s, f i) * ∏ i ∈ s, (1 - (q ^ f i)⁻¹).

theorem Finset.sum_range_add_mul_add_div_two {K : Type u_1} [Field K] [CharZero K] (a u X : K) (n : ℕ) : ∑ k ∈ range n, (a * u + (↑k * a + a / 2) * a * X) = ↑n * a * u + (↑n * a) ^ 2 * X / 2

The expected increments a * u + (k * a + a / 2) * a * X of the quadratic t ↦ t * u + t ^ 2 * X / 2 along the grid k * a sum, over k < n, to the increment n * a * u + (n * a) ^ 2 * X / 2 of the quadratic from 0 to n * a.