Ssreflect Users Discussion List

[Georges Gonthier <>]

     rewrite -big_filter filter_index_enum will do the trick.
 (Yes, you sometimes need to use rewrite rules in the converse direction...).

  Cheers,
Georges

-----Original Message-----
From:  [] 
Sent: 15 June 2011 11:13
To: ssreflect
Subject: switching between big ops on sets and big ops on sequences

I have a big op on a set similar to:

  \prod_(i \in s) ('X - (s a)%:P)

s is some subset of an automorphism group.

I want to convert this into

\prod_(i <- enum s) ('X - (s a)%:P)

in order to apply my lemma that such a product would be a separable (aka 
square free) polynomial (since (enum s) is uniq).

However, I can't find any lemma to do such a conversion.  big_uniq comes 
close, but I can't get it to work.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone 
Company wrote, ``is the merest claptrap, for there exists no property in 
ideas musical, literary or artistic, except as defined by statute.''