# Zulip Chat Archive

## Stream: maths

### Topic: product of 0s and 1s

#### Reid Barton (Oct 24 2019 at 00:33):

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 (Oct 24 2019 at 00:35):

I think that should be exists instead of forall?

#### Mario Carneiro (Oct 24 2019 at 00:35):

or 0 and 1 should be swapped

#### Reid Barton (Oct 24 2019 at 00:37):

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

#### Mario Carneiro (Oct 24 2019 at 00:37):

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 (Oct 24 2019 at 00:38):

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

#### Mario Carneiro (Oct 24 2019 at 00:39):

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

to `a ^ card s`

first

#### Reid Barton (Oct 24 2019 at 00:40):

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 (Oct 24 2019 at 00:41):

at some point it becomes theorem-local reasoning though

#### Mario Carneiro (Oct 24 2019 at 00:41):

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

#### Reid Barton (Oct 24 2019 at 00:42):

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

#### Kenny Lau (Oct 24 2019 at 00:42):

`finset.prod_filter`

, `finset.prod_const`

, `zero_pow`

/ `pow_zero`

#### Mario Carneiro (Oct 24 2019 at 00:42):

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

#### Mario Carneiro (Oct 24 2019 at 00:42):

these are all equalities

#### Mario Carneiro (Oct 24 2019 at 00:44):

I think I just rationally reconstructed mathlib

#### Reid Barton (Oct 24 2019 at 00:47):

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 (Oct 24 2019 at 00:47):

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 (Oct 24 2019 at 00:48):

I think that's the right conclusion

#### Kenny Lau (Oct 24 2019 at 00:48):

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 (Oct 24 2019 at 00:49):

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

?

Last updated: May 11 2021 at 15:12 UTC