ssreflect - [ssreflect] bigop in abelian subsets

Subject: Ssreflect Users Discussion List

List archive

[ssreflect] bigop in abelian subsets

From: Florent Hivert <>
To: "" <>
Cc: Thibaut Benjamin <>
Subject: [ssreflect] bigop in abelian subsets
Date: Mon, 18 Apr 2016 17:59:17 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=None ; spf=None
Ironport-phdr: 9a23:PwO+wR+5WViqk/9uRHKM819IXTAuvvDOBiVQ1KB80+8cTK2v8tzYMVDF4r011RmSDdWdtagP2raempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lSsiM1Y/mi6ibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwuwwZgf8q9tZBXKPmZOx4COUAVHV1e1wysYfwrgPOQw+C7Wc0V34M1xtOGQnMqhD8RJb49CXg/KIpwzKAMMPyQLsocTG59eJqTgXpgWEGMSQ4+SfZkJojorhcpUePoxtlzojIKKGUKvdkYuuJU9cdX2dHQoBxVjJMGJ+Ua5EOSeQba7UL57LhrkcD+EPtTTKnA/nin3oR3if7

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

[ssreflect] bigop in abelian subsets, Florent Hivert, 04/18/2016
- Re: [ssreflect] bigop in abelian subsets, Emilio Jesús Gallego Arias, 04/18/2016
  - Re: [ssreflect] bigop in abelian subsets, Emilio Jesús Gallego Arias, 04/18/2016
- RE: [ssreflect] bigop in abelian subsets, Georges Gonthier, 04/18/2016
  - RE: [ssreflect] bigop in abelian subsets, Georges Gonthier, 04/19/2016
    - Re: [ssreflect] bigop in abelian subsets, Florent Hivert, 04/19/2016

List archive

[ssreflect] bigop in abelian subsets