Ssreflect Users Discussion List

[Georges Gonthier <>]

  Dear Florent,
The most comfortable to do this is to use the facilities provided by 
finmodule.v for injecting elements of an abelian group A into a finite 
(Z-)module. The fmval projection out maps sums in fmod_of abelA (where ableA 
: abelian A) to group products, so you can comfortably do all your algebra 
with full ssralg support in the module, then translate back to 'S_n.
    Best,
Georges

-----Original Message-----
From: 

 
[mailto:]
 On Behalf Of Florent Hivert
Sent: 18 April 2016 16:59
To: 

Cc: Thibaut Benjamin 
<>
Subject: [ssreflect] bigop in abelian subsets

      Dear all,

I'm working in 'S_n which is a non abelian groups. I have a set A of element 
of 'S_n which I know is abelian. I'd like use rewriting bigop lemmas such as

  Lemma big_setD1 a A F : a \in A ->
    \big[aop/idx]_(i in A) F i = aop (F a) (\big[aop/idx]_(i in A :\ a) F i).

to expression such as

   \prod_(s \in A) s

However big_setD1 requires a Monoid.com_law. Commutation is only valid in the 
subgroup <<A>> generated by A. Is there an easy way to localize the product 
in <<A>> to use commutation ?

Best,

Florent