Sums through linear maps and into a product

Two small families used wherever a coordinate computation pushes a finite sum through a bound map and then splits it across the summands of a product: map_sum/map_zero at a bound linear map or equivalence, and the four ways a sum can sit in A × B.

They are stated for bound maps because simp will not otherwise rewrite under a LinearMap applied to a Finset.sum, and they live here rather than beside their first user because two files need them.

theorem RS.equiv_sum {M : Type u_1} {N : Type u_2} {ι : Type u_5} [AddCommMonoid M] [Module ℂ M] [AddCommMonoid N] [Module ℂ N] (e : M ≃ₗ[ℂ] N) (s : Finset ι) (f : ι → M) : e (∑ i ∈ s, f i) = ∑ i ∈ s, e (f i)

map_sum for a bound linear equivalence.

theorem RS.equiv_add {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module ℂ M] [AddCommMonoid N] [Module ℂ N] (e : M ≃ₗ[ℂ] N) (x y : M) : e (x + y) = e x + e y

map_add for a bound linear equivalence.

theorem RS.lmap_sum {M : Type u_1} {N : Type u_2} {ι : Type u_5} [AddCommMonoid M] [Module ℂ M] [AddCommMonoid N] [Module ℂ N] (f : M →ₗ[ℂ] N) (s : Finset ι) (g : ι → M) : f (∑ i ∈ s, g i) = ∑ i ∈ s, f (g i)

map_sum for a bound linear map.

theorem RS.lmap_zero {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module ℂ M] [AddCommMonoid N] [Module ℂ N] (f : M →ₗ[ℂ] N) : f 0 = 0

map_zero for a bound linear map.

theorem RS.mk_add_left {A : Type u_3} {B : Type u_4} [AddCommMonoid A] [AddCommMonoid B] (a a' : A) : (a + a', 0) = (a, 0) + (a', 0)

Addition in the left summand of a product.

theorem RS.mk_add_right {A : Type u_3} {B : Type u_4} [AddCommMonoid A] [AddCommMonoid B] (b b' : B) : (0, b + b') = (0, b) + (0, b')

Addition in the right summand.

theorem RS.mk_sum_left {A : Type u_3} {B : Type u_4} {ι : Type u_5} [AddCommMonoid A] [AddCommMonoid B] (s : Finset ι) (f : ι → A) : (∑ i ∈ s, f i, 0) = ∑ i ∈ s, (f i, 0)

A sum in the left summand.

theorem RS.mk_sum_right {A : Type u_3} {B : Type u_4} {ι : Type u_5} [AddCommMonoid A] [AddCommMonoid B] (t : Finset ι) (g : ι → B) : (0, ∑ j ∈ t, g j) = ∑ j ∈ t, (0, g j)

A sum in the right summand.

theorem RS.mk_sum_split {A : Type u_3} {B : Type u_4} {ι : Type u_5} {κ : Type u_6} [AddCommMonoid A] [AddCommMonoid B] (s : Finset ι) (t : Finset κ) (f : ι → A) (g : κ → B) : (∑ i ∈ s, f i, ∑ j ∈ t, g j) = ∑ i ∈ s, (f i, 0) + ∑ j ∈ t, (0, g j)

A pair of sums splits into the two summands' sums — the shape the even and odd blocks are computed in.