Zulip Chat Archive

Stream: general

Topic: sum ite over fin


Johan Commelin (Sep 07 2018 at 13:53):

How do I kill off this one?

lemma MWE (R : Type v) [ring R] (n : ) :
finset.univ.sum (λ (k : fin (n + 2)), (-1) ^ k.val * ite (0 = k) (1 : R) (0 : R)) = 1 := sorry

Chris Hughes (Sep 07 2018 at 13:58):

finset.sum_eq_single

Kenny Lau (Sep 07 2018 at 13:59):

not found

Kenny Lau (Sep 07 2018 at 14:00):

import data.fintype

universe v

lemma MWE (R : Type v) [ring R] (n : ) :
finset.univ.sum (λ (k : fin (n + 2)), (-1) ^ k.val * ite (0 = k) (1 : R) (0 : R)) = 1 :=
begin
  transitivity finset.sum (finset.singleton 0 : finset (fin (n+2))) _,
  { symmetry,
    apply finset.sum_subset,
    { intros i H, simp },
    { intros, simp at a, simp [ne.symm a] } },
  simp, refl
end

Chris Hughes (Sep 07 2018 at 14:00):

It's actually sum_eq_single due to a naming error.

Kenny Lau (Sep 07 2018 at 14:00):

that's the same thing, and still not found

Johan Commelin (Sep 07 2018 at 14:00):

@Chris Hughes My Lean still doesn't find it.

Chris Hughes (Sep 07 2018 at 14:07):

I think it might be new.


Last updated: Dec 20 2023 at 11:08 UTC