diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-06-16 15:51:26 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-06-16 15:51:26 -0400 |
commit | 26640780a5cdce3aed531c1bf7cdaa692244edc7 (patch) | |
tree | 409e8f62beebf8416a98f5505e3e38c0a7f450fe /src/ModularArithmetic/ModularArithmeticTheorems.v | |
parent | a5f12b2990047847cff78424b8b62330bad67454 (diff) |
Z is integral domain
Diffstat (limited to 'src/ModularArithmetic/ModularArithmeticTheorems.v')
-rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index dabfcf883..fe7600784 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -149,6 +149,16 @@ Section FandZ. intuition; find_inversion; rewrite ?Z.mod_0_l, ?Z.mod_small in *; intuition. Qed. + Require Crypto.Algebra. + Global Instance ring_modulo : @Algebra.ring (F m) Logic.eq (ZToField 0) (ZToField 1) opp add sub mul. + Proof. + repeat split; Fdefn. + { rewrite Z.add_0_r. auto. } + { rewrite <-Z.add_sub_swap, <-Z.add_sub_assoc, Z.sub_diag, Z.add_0_r. apply Z_mod_same_full. } + { apply F_eq_dec. } + { rewrite Z.mul_1_r. auto. } + Qed. + Lemma ZToField_0 : @ZToField m 0 = 0. Proof. Fdefn. |