## Stream: Is there code for X?

### Topic: finset.sum_apply'

#### Kenny Lau (May 25 2020 at 10:13):

import data.finsupp

universes u v w

variables {α : Type u} {ι : Type v} {β : Type w} [add_comm_group β]
variables {s : finset α} {f : α → (ι →₀ β)} (i : ι)

theorem finset.sum_apply' : (s.sum f) i = s.sum (λ x, f x i) :=
sorry


#### Mario Carneiro (May 25 2020 at 10:13):

looks like a sum hom theorem to me

#### Kenny Lau (May 25 2020 at 10:13):

the (sum of a bunch of finitely supported functions) applied to an element is the sum of (the functions applied to the element)

#### Kenny Lau (May 25 2020 at 10:13):

but should this be in the library separately?

#### Mario Carneiro (May 25 2020 at 10:14):

If you can get it to be a literal application of sum_hom and some apply_add_hom theorem then I would say no

#### Kenny Lau (May 25 2020 at 10:17):

import data.finsupp

universes u v w

variables {α : Type u} {ι : Type v} {β : Type w} [add_comm_group β]
variables {s : finset α} {f : α → (ι →₀ β)} (i : ι)

theorem finset.sum_apply' : (s.sum f) i = s.sum (λ x, f x i) :=
(s.sum_hom $λ g : ι →₀ β, g i).symm  #### Kenny Lau (May 25 2020 at 10:17): well in practice \io might be a huge term #### Kenny Lau (May 25 2020 at 10:17): (it is in my use case) #### Kenny Lau (May 25 2020 at 10:20): and also i is a huge term #### Kenny Lau (May 25 2020 at 10:22): and I run into coe_fn problems function expected at f term has type ↥↑(finset.map (mul_action.to_fun G F) s) →₀ F  #### Mario Carneiro (May 25 2020 at 10:25): #mwe? #### Mario Carneiro (May 25 2020 at 10:25): or at least context #### Kevin Buzzard (May 25 2020 at 10:28): #### Kenny Lau (May 25 2020 at 10:36): import algebra.group_ring_action linear_algebra.dimension field_theory.subfield universes u v variables (G : Type u) [group G] (F : Type v) [field F] [mul_semiring_action G F] (g : G) def fixed : set F := { x | ∀ g : G, g • x = x } instance : is_subfield (fixed G F) := sorry /-- Embedding induced by action. -/ def mul_action.to_fun : F ↪ (G → F) := ⟨λ x m, m • x, λ x y H, one_smul G x ▸ one_smul G y ▸ by convert congr_fun H 1⟩ theorem linear_independent_smul_of_linear_independent {s : finset F} (i : F) (his : i ∈ s) : (@finset.sum _ ((↑(s.map$ mul_action.to_fun G F) : set (G → F)) →₀ F) _ s.attach
(λ i, finsupp.single ⟨_, finset.mem_map_of_mem _ i.2⟩ (g • i.1 - i.1)))
⟨_, finset.mem_map_of_mem _ his⟩ = 0 :=
by rw ← s.attach.sum_hom (λ f : (↑(s.map \$ mul_action.to_fun G F) : set (G → F)) →₀ F, f ⟨mul_action.to_fun G F i, finset.mem_map_of_mem _ his⟩)


#### Yury G. Kudryashov (May 25 2020 at 16:04):

Look at finset_prod_apply in algebra/pi_instances

#### Yury G. Kudryashov (May 25 2020 at 16:04):

@[to_additive] automatically declares finset_sum_apply

Last updated: May 17 2021 at 15:13 UTC