Zulip Chat Archive

Stream: Is there code for X?

Topic: union of list of finsets


view this post on Zulip Kenny Lau (Jul 28 2020 at 08:39):

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

view this post on Zulip Johan Commelin (Jul 28 2020 at 08:40):

How did you end up with a list?

view this post on Zulip 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 ()  :=

view this post on Zulip Johan Commelin (Jul 28 2020 at 08:40):

(deleted)

view this post on Zulip Kenny Lau (Jul 28 2020 at 08:41):

I actually need this for multiset

view this post on Zulip Mario Carneiro (Jul 28 2020 at 08:41):

wouldn't sup work?

view this post on Zulip Johan Commelin (Jul 28 2020 at 08:41):

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

view this post on Zulip Kenny Lau (Jul 28 2020 at 08:42):

maybe I should name it p instead of x

view this post on Zulip Kenny Lau (Jul 28 2020 at 08:42):

Mario Carneiro said:

wouldn't sup work?

list.sup?

view this post on Zulip Johan Commelin (Jul 28 2020 at 08:42):

Yes, maybe you should

view this post on Zulip Johan Commelin (Jul 28 2020 at 08:42):

Or f, or \phi. But not x

view this post on Zulip Mario Carneiro (Jul 28 2020 at 08:43):

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

view this post on Zulip Kenny Lau (Jul 28 2020 at 08:44):

no

view this post on Zulip Mario Carneiro (Jul 28 2020 at 08:44):

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

view this post on Zulip Kenny Lau (Jul 28 2020 at 08:44):

yes, but let's work with finset for now

view this post on Zulip Kenny Lau (Jul 28 2020 at 08:47):

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

view this post on Zulip Mario Carneiro (Jul 28 2020 at 08:51):

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

view this post on Zulip Kenny Lau (Jul 28 2020 at 08:53):

touché


Last updated: May 17 2021 at 15:13 UTC