diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-01 23:59:55 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-02 00:00:09 -0400 |
commit | d3135a69f653034f07b7657486f926a7a20ef3ee (patch) | |
tree | e163e017643c1bc8c877ecefaa43299c458d232e /coqprime/Coqprime/FGroup.v | |
parent | 3f11f57487ce9e913b36271cee2f8b6b695945cf (diff) |
Strip trailing whitespace
With
```bash
bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh
```
Diffstat (limited to 'coqprime/Coqprime/FGroup.v')
-rw-r--r-- | coqprime/Coqprime/FGroup.v | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/coqprime/Coqprime/FGroup.v b/coqprime/Coqprime/FGroup.v index a55710e7c..ee18761ab 100644 --- a/coqprime/Coqprime/FGroup.v +++ b/coqprime/Coqprime/FGroup.v @@ -7,22 +7,22 @@ (*************************************************************) (********************************************************************** - FGroup.v - - Defintion and properties of finite groups - - Definition: FGroup + FGroup.v + + Defintion and properties of finite groups + + Definition: FGroup **********************************************************************) Require Import List. Require Import UList. Require Import Tactic. Require Import ZArith. -Open Scope Z_scope. +Open Scope Z_scope. Set Implicit Arguments. -(************************************** +(************************************** A finite group is defined for an operation op it has a support (s) op operates inside the group (internal) @@ -32,7 +32,7 @@ Set Implicit Arguments. the inverse operates inside the group (i_internal) it gives an inverse (i_is_inverse_l is_is_inverse_r) **************************************) - + Record FGroup (A: Set) (op: A -> A -> A): Set := mkGroup {s : (list A); unique_s: ulist s; @@ -48,10 +48,10 @@ Record FGroup (A: Set) (op: A -> A -> A): Set := mkGroup i_is_inverse_r: forall a, (In a s) -> op a (i a) = e }. -(************************************** +(************************************** The order of a group is the lengh of the support **************************************) - + Definition g_order (A: Set) (op: A -> A -> A) (g: FGroup op) := Z_of_nat (length g.(s)). Unset Implicit Arguments. @@ -65,7 +65,7 @@ Section FGroup. Variable A: Set. Variable op: A -> A -> A. -(************************************** +(************************************** Some properties of a finite group **************************************) @@ -91,7 +91,7 @@ apply sym_equal; apply assoc with g; sauto. replace (op a (g.(i) a)) with g.(e); sauto. Qed. -Theorem e_unique: forall (g : FGroup op), forall e1, In e1 g.(s) -> (forall a, In a g.(s) -> op e1 a = a) -> e1 = g.(e). +Theorem e_unique: forall (g : FGroup op), forall e1, In e1 g.(s) -> (forall a, In a g.(s) -> op e1 a = a) -> e1 = g.(e). intros g e1 He1 H2. apply trans_equal with (op e1 g.(e)); sauto. Qed. @@ -110,7 +110,7 @@ intro g; apply g_cancel_l with (g:= g) (a := g.(e)); sauto. apply trans_equal with g.(e); sauto. Qed. -(************************************** +(************************************** A group has at least one element **************************************) |