diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-24 18:06:57 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-24 18:06:57 -0400 |
| commit | 61bdcf3de1f506907d62a2a7c32594c1a666d474 (patch) | |
| tree | 66e8d5ef7153cc9cd404895c23b20a2d44bbfc55 /src/Algebra.v | |
| parent | 7488addb5938b203d1c9402908cc9b440d9573b6 (diff) | |
ExtendedCoordinates: group.
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index a46b010b5..ecc5e4209 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -292,9 +292,9 @@ Module Group. {Proper_inv:Proper(eq==>eq)inv} {phi iph} {Proper_phi:Proper(EQ==>eq)phi} {Proper_iph:Proper(eq==>EQ)iph} {surj:forall h, phi (iph h) = h} - {phi_op : forall a b, phi (OP a b) = op (phi a) (phi b)} - {phi_inv : forall a, phi (INV a) = inv (phi a)} - {phi_id : phi ID = id} + {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))} + {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))} + {phi_id : eq (phi ID) id} : @group H eq op id inv. Proof. repeat split; eauto with core typeclass_instances; intros; @@ -318,9 +318,9 @@ Module Group. {H eq op id inv} {groupG:@group H eq op id inv} {phi} {eq_phi_EQ: forall x y, eq (phi x) (phi y) -> EQ x y} - {phi_op : forall a b, phi (OP a b) = op (phi a) (phi b)} - {phi_inv : forall a, phi (INV a) = inv (phi a)} - {phi_id : phi ID = id} + {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))} + {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))} + {phi_id : eq (phi ID) id} : @group G EQ OP ID INV. Proof. repeat split; eauto with core typeclass_instances; intros; |