diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-20 14:35:46 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-20 14:35:46 -0400 |
| commit | a0bdb14300aa57eed684992a23a57fd319ef97c0 (patch) | |
| tree | a2a57d84ecfe9c75578d26cfda57dd0fbe840151 /src/Algebra.v | |
| parent | 1a5130702303e2843ab458e2566bef293c6947cd (diff) | |
Algebra: change a aliasing definition into an aliasing lemma to appease implicit argument resolution
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index b8cc3c921..6dc188e2c 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -378,8 +378,8 @@ Module Ring. Context `{is_homomorphism}. - Definition homomorphism_add : forall x y, phi (ADD x y) = add (phi x) (phi y) := - Group.homomorphism. + Lemma homomorphism_add : forall x y, phi (ADD x y) = add (phi x) (phi y). + Proof. apply Group.homomorphism. Qed. Definition homomorphism_opp : forall x, phi (OPP x) = opp (phi x) := (Group.homomorphism_inv (INV:=OPP) (inv:=opp)). |