Stream: math-comp users

Topic: Group theory related theorem proving by coq.

view this post on Zulip Hongyi Zhao (May 06 2022 at 01:39):

How can I formulate the rearrangement theorem [1] and then prove it, by coq?

[1] https://mathworld.wolfram.com/RearrangementTheorem.html

Regards
HZ

view this post on Zulip Laurent Théry (May 06 2022 at 12:48):

There are several ways to formulate this property.
Maybe one that is close enough to Wolfram formulation is 

From mathcomp Require Import all_ssreflect all_fingroup.

Variable gT : finGroupType.
Variable G : {group gT}.

Lemma rearrangement x :
 x \in G -> perm_eq [seq i | i in G] [seq (x * i)%g | i in G].

it requires some expertise about perm_eq to prove but it is a consequence of the theorem mulgI.

Last updated: Feb 08 2023 at 07:02 UTC