Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Hi Florent,

after thinking a bit more, I think it is better if you'd disregard my
precipitated suggestion for now as there is for sure a better way.

Sorry for the noise,
E.


 (Emilio Jesús Gallego Arias) writes:

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