fintype.prod_dite

Stream: new members

[Alex Zhang]

Why doesn't fintype.prod_dite has the label to_additive? I need to use the sum version of this. :cry:

[Alex Zhang]

and an ite version also seems missing

[Alex Zhang]

Not very familiar with this part, I would be grateful if anyone can do the poof!

@[to_additive]
lemma fintype.prod_ite [fintype α] {p : α → Prop} [decidable_pred p]
  [comm_monoid β] (f g : α → β) :
  (∏ a, ite (p a) (f a) (g a)) = (∏ a : {a // p a}, f a) * (∏ a : {a // ¬p a}, g a) :=
begin
  simp only [finset.prod_ite, finset.attach_eq_univ],
  congr' 1,
  { library_search},
  { sorry }
end

[Yakov Pechersky]

Please, #mwe with imports and variables

[Yakov Pechersky]

You have that already, and for us to try to explore the issue, we'd have to rewrite it ourselves. It's almost surely easier for you to just copy+paste the extra few lines

[Alex Zhang]

import algebra.big_operators
open_locale big_operators
variables {α β : Type*}

@[to_additive]
lemma fintype.prod_ite [fintype α] {p : α → Prop} [decidable_pred p]
  [comm_monoid β] (f g : α → β) :
  (∏ a, ite (p a) (f a) (g a)) = (∏ a : {a // p a}, f a) * (∏ a : {a // ¬p a}, g a) :=
begin
  simp only [finset.prod_ite, finset.attach_eq_univ],
  congr' 1,
  { sorry},
  { sorry}
end

[Alex Zhang]

I wrote the imports.

[Yakov Pechersky]

I tagged fintype.prod_dite at @{to_additive] in data.fintype.card and then the following works:

import data.fintype.card

open_locale big_operators

variables {α β : Type*}

@[to_additive]
lemma fintype.prod_ite [fintype α] {p : α → Prop} [decidable_pred p]
  [comm_monoid β] (f g : α → β) :
  (∏ a, ite (p a) (f a) (g a)) = (∏ a : {a // p a}, f a) * (∏ a : {a // ¬p a}, g a) :=
fintype.prod_dite _ _

#check fintype.sum_ite

[Alex Zhang]

I think this can make a PR.

[Yakov Pechersky]

Feel free to!

[Alex Zhang]

Can this be made more general? @Yakov Pechersky

[Yakov Pechersky]

Well the dite version is the more general one, no? What additional generality would you want?

[Yakov Pechersky]

By the way, in the {prod,sum}_ite lemma, p should be an explicit variable.

[Alex Zhang]

I am not sure if there could be any generalization. I was just asking. This lemma now is enough for my own use.