Collapsing an iterated product of powers into a single product of powers

Finset.prod_pow_eq_pow_sum collapses a product of natural powers of one fixed element into a single power. This file records the analogue for integral powers, in a commutative group and in a commutative group with zero at an invertible element, and the three substitution rules that follow from it: substituting a family of monomials into a monomial multiplies the two exponent matrices.

These are the bookkeeping rules behind composing monomial maps in coordinates, where the exponent matrices may carry natural or integral entries depending on whether the coordinate they act on is allowed to vanish.

Main results

• Finset.prod_zpow_eq_zpow_sum and Finset.prod_zpow_eq_zpow_sum₀: ∏ i ∈ s, y ^ e i = y ^ ∑ i ∈ s, e i, in a commutative group and, for y ≠ 0, in a commutative group with zero.
• Finset.prod_prod_pow, Finset.prod_prod_zpow and Finset.prod_prod_zpow_pow: substituting monomials into a monomial multiplies the exponent matrices, for the three combinations of natural and integral exponents that make sense.

theorem Finset.prod_zpow_eq_zpow_sum {ι : Type u_1} {G : Type u_4} [CommGroup G] (s : Finset ι) (y : G) (e : ι → ℤ) : ∏ i ∈ s, y ^ e i = y ^ ∑ i ∈ s, e i

A product of integral powers of one fixed element of a commutative group collapses to a single power. This is the integral-exponent analogue of Finset.prod_pow_eq_pow_sum.

theorem Finset.prod_zpow_eq_zpow_sum₀ {ι : Type u_1} {G₀ : Type u_5} [CommGroupWithZero G₀] (s : Finset ι) {y : G₀} (hy : y ≠ 0) (e : ι → ℤ) : ∏ i ∈ s, y ^ e i = y ^ ∑ i ∈ s, e i

A product of integral powers of one fixed invertible element of a commutative group with zero collapses to a single power.

theorem Finset.prod_prod_pow {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [CommMonoid M] (s : Finset ι) (t : Finset κ) (x : κ → M) (e : ι → κ → ℕ) (g : ι → ℕ) : ∏ a ∈ s, (∏ b ∈ t, x b ^ e a b) ^ g a = ∏ b ∈ t, x b ^ ∑ a ∈ s, g a * e a b

Substituting the monomials ∏ b ∈ t, x b ^ e a b into the monomial with natural exponents g produces the monomial whose exponent matrix is the product ∑ a ∈ s, g a * e a b.

theorem Finset.prod_prod_zpow {ι : Type u_1} {κ : Type u_2} {G₀ : Type u_5} [CommGroupWithZero G₀] (s : Finset ι) (t : Finset κ) {y : κ → G₀} (hy : ∀ b ∈ t, y b ≠ 0) (e : ι → κ → ℤ) (g : ι → ℤ) : ∏ a ∈ s, (∏ b ∈ t, y b ^ e a b) ^ g a = ∏ b ∈ t, y b ^ ∑ a ∈ s, g a * e a b

Substituting the monomials ∏ b ∈ t, y b ^ e a b in invertible coordinates into the monomial with integral exponents g produces the monomial whose exponent matrix is the product ∑ a ∈ s, g a * e a b.

theorem Finset.prod_prod_zpow_pow {ι : Type u_1} {κ : Type u_2} {G₀ : Type u_5} [CommGroupWithZero G₀] (s : Finset ι) (t : Finset κ) {y : κ → G₀} (hy : ∀ b ∈ t, y b ≠ 0) (e : ι → κ → ℤ) (g : ι → ℕ) : ∏ a ∈ s, (∏ b ∈ t, y b ^ e a b) ^ g a = ∏ b ∈ t, y b ^ ∑ a ∈ s, ↑(g a) * e a b

The mixed case of Finset.prod_prod_zpow: monomials with integral exponents in invertible coordinates, substituted into a monomial with natural exponents g.