Ssreflect Users Discussion List

[Georges Gonthier <>]

 Unfortunately, this isn't directly supported by the bigop library. There is 
an indirect way of achieving this if the submonoid on which the operator is 
commutative can be characterized, by mapping the product to the corresponding 
subtype, where the Abelian part of bigop can be used freely.
This is done for instance for the proof of the Schur-Zassenhaus and transfer 
theorems in finmodule.v (going from a finite abelian subgroup to a finite 
module).
  If this doesn't make sense in your proof you'll likely be better off 
redoing part of the Abelian section under a weaker assumption, such as
   commutative (fun i j => F i * F j).
for instance proving bigD1, then deriving reindex_onto and reindex (in bigop 
bigD1 is derived from big_split, but that involves changing the general term 
F, which wouldn't work for the assumption above).

Sorry,
   Georges

-----Original Message-----
From:  
[] On Behalf Of Laurence Rideau
Sent: 11 June 2014 17:25
To: 
Cc: Sophie Bernard
Subject: [ssreflect] bigop question

Hello,
we need to reindex a bigop, where  elements commute  pariwise (but the 
underlying operator is not commutative in general).

Do you have an idea to help us?

Thanks
laurence