product of 0s and 1s

Stream: maths

[Reid Barton]

Is there already a lemma like s.prod (\lam i, if p i then 0 else 1) = if (\forall i \in s, p i) then 0 else 1?

[Mario Carneiro]

I think that should be exists instead of forall?

[Mario Carneiro]

or 0 and 1 should be swapped

[Reid Barton]

Yes exists, sorry, or any other similar but correct statement

[Mario Carneiro]

I would prefer to see that factored into s.prod (\lam i, if p i then f i else 0) = (s.filter p).prod f and s.prod (\lam _, 1) = if s != \empty then 1 else 0

[Mario Carneiro]

I'm not a big fan of if statements in conclusions though; I would probably state the latter as two lemmas

[Mario Carneiro]

It might also make sense to add an additional step that connects s.prod (\lam _, a) to a ^ card s first

[Reid Barton]

In the intended application (https://en.wikipedia.org/wiki/Chevalley%E2%80%93Warning_theorem#Proof_of_Warning's_theorem) you do kind of want the if ... then 1 else 0 form though, since another lemma connects the sum of that to the cardinality of a set.

[Mario Carneiro]

at some point it becomes theorem-local reasoning though

[Mario Carneiro]

I would just use funext and split_ifs to get the if back

[Reid Barton]

You people don't like if and only if statements, do you

[Kenny Lau]

finset.prod_filter, finset.prod_const, zero_pow / pow_zero

[Mario Carneiro]

I'm a big fan of iff statements, what do you mean?

[Mario Carneiro]

these are all equalities

[Mario Carneiro]

I think I just rationally reconstructed mathlib

[Reid Barton]

Each term is the product of the indicator functions of $f_i(x) = 0$, which is the indicator function of $\forall i, f_i(x) = 0$, and summing that gives the number of solutions. I don't want to separately argue when all $f_i(x)$ are zero and when some $f_i(x)$ is not zero.

[Reid Barton]

Maybe I am just arguing that the function we talked about in #1472 should exist, and not fall under the general rule about ifs in conclusions.

[Mario Carneiro]

I think that's the right conclusion

[Kenny Lau]

import data.finsupp

universes u v

example (α : Type u) (β : Type v) [comm_ring β] (s : finset α) (p : α → Prop) [decidable_pred p] :
  s.prod (λ i, if p i then 0 else 1) = if ∃ i ∈ s, p i then 0 else 1 :=
by rw [← finset.prod_filter, finset.prod_const]
-- ⊢ 0 ^ finset.card (finset.filter (λ (a : α), p a) s) = ite (∃ (i : α) (H : i ∈ s), p i) 0 1

[Kenny Lau]

maybe 0 ^ finset.card (finset.filter (λ (a : α), p a) s)?