Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Hi Florent,

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

Others will without doubt offer a better solution, and my proposal
doesn't quality as "easy", but let me suggest that you try to generalize
the `big_split` lemma in a similar manner to what is done in `can_in_inj`
etc...

Something like {in <<A>> &, commutative op} should do the trick.

[Sorry, I didn't have time today to try it myself]
E.