diff options
author | Jason Gross <jgross@mit.edu> | 2016-09-30 12:54:09 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-09-30 12:54:09 -0400 |
commit | 6fadbfa7814900332604688a787b0214dc30761e (patch) | |
tree | 1223e22f7a1a7795d86928e44b08e4f76802418f /src | |
parent | b59651f1fb0128def9a696af7082fc8cc9933d17 (diff) |
Weaken surjective_homomorphism_from_group
We shouldn't be talking about leibniz equality in groups
Diffstat (limited to 'src')
-rw-r--r-- | src/Algebra.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index 0c27395f8..5239aae33 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -313,7 +313,7 @@ Module Group. {Proper_op:Proper(eq==>eq==>eq)op} {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} + {surj:forall h, eq (phi (iph h)) h} {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} |