Zulip Chat Archive

Stream: Is there code for X?

Topic: finset.sum_apply'


view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 25 2020 at 10:13):

looks like a sum hom theorem to me

view this post on Zulip 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)

view this post on Zulip Kenny Lau (May 25 2020 at 10:13):

but should this be in the library separately?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 25 2020 at 10:17):

well in practice \io might be a huge term

view this post on Zulip Kenny Lau (May 25 2020 at 10:17):

(it is in my use case)

view this post on Zulip Kenny Lau (May 25 2020 at 10:20):

and also i is a huge term

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 25 2020 at 10:25):

#mwe?

view this post on Zulip Mario Carneiro (May 25 2020 at 10:25):

or at least context

view this post on Zulip Kevin Buzzard (May 25 2020 at 10:28):

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

view this post on Zulip 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)

view this post on Zulip Yury G. Kudryashov (May 25 2020 at 16:04):

Look at finset_prod_apply in algebra/pi_instances

view this post on Zulip 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