## Stream: Is there code for X?

### Topic: union of list of finsets

#### Kenny Lau (Jul 28 2020 at 08:39):

What is the idiomatic way to take union of a list of finsets? L.foldl (∪) ∅?

#### Johan Commelin (Jul 28 2020 at 08:40):

How did you end up with a list?

#### Kenny Lau (Jul 28 2020 at 08:40):

theorem roots_list_prod {R : Type*} [integral_domain R] (L : list (polynomial R)) :
(∀ x ∈ L, (x : _) ≠ 0) → L.prod.roots = (L.map roots).foldl (∪) ∅ :=


(deleted)

#### Kenny Lau (Jul 28 2020 at 08:41):

I actually need this for multiset

#### Mario Carneiro (Jul 28 2020 at 08:41):

wouldn't sup work?

#### Johan Commelin (Jul 28 2020 at 08:41):

Whut? Why x \in L if L is a list of polynomials??

#### Kenny Lau (Jul 28 2020 at 08:42):

maybe I should name it p instead of x

#### Kenny Lau (Jul 28 2020 at 08:42):

Mario Carneiro said:

wouldn't sup work?

list.sup?

#### Johan Commelin (Jul 28 2020 at 08:42):

Yes, maybe you should

#### Johan Commelin (Jul 28 2020 at 08:42):

Or f, or \phi. But not x

#### Mario Carneiro (Jul 28 2020 at 08:43):

Is there a definition of the multiset of roots of a polynomial?

no

#### Mario Carneiro (Jul 28 2020 at 08:44):

it might be better to prove that this is an equality of multisets, not just finsets

#### Kenny Lau (Jul 28 2020 at 08:44):

yes, but let's work with finset for now

#### Kenny Lau (Jul 28 2020 at 08:47):

ok I have decided that the idiomatic way is L.to_finset.bind id

#### Mario Carneiro (Jul 28 2020 at 08:51):

I guess in your case it could be L.to_finset.bind roots

#### Kenny Lau (Jul 28 2020 at 08:53):

touché

Last updated: May 17 2021 at 15:13 UTC