finset.sum_apply'

Stream: Is there code for X?

[Kenny Lau]

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]

looks like a sum hom theorem to me

[Kenny Lau]

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]

but should this be in the library separately?

[Mario Carneiro]

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]

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]

well in practice \io might be a huge term

[Kenny Lau]

(it is in my use case)

[Kenny Lau]

and also i is a huge term

[Kenny Lau]

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]

#mwe?

[Mario Carneiro]

or at least context

[Kevin Buzzard]

Maybe https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/slow.20elaboration/near/198648425 is related?

[Kenny Lau]

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]

Look at finset_prod_apply in algebra/pi_instances

[Yury G. Kudryashov]

@[to_additive] automatically declares finset_sum_apply