Zulip Chat Archive

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 (∪) ∅ :=

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

(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?

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

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: Dec 20 2023 at 11:08 UTC