diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-07-28 18:40:28 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-08-04 11:47:51 -0400 |
commit | 4964f1ff2d40ba08573deddca56140c4ac4b19eb (patch) | |
tree | 61b24623e414dfa3e09a32cf62e8acd1909dae37 /src/Util/NumTheoryUtil.v | |
parent | fbb0f64892560322ed9dcd0f664e730e74de9b4e (diff) |
Refactor ModularArithmetic into Zmod, expand Decidable
ModularArithmetic now uses Algebra lemmas in various places instead of
custom manual proofs. Similarly, Util.Decidable is used to state and
prove the relevant decidability results.
Backwards-incompatible changes:
F_some_lemma -> Zmod.some_lemma
Arguments ZToField _%Z _%Z : clear implicits.
inv_spec says inv x * x = 1, not x * inv x = 1
Diffstat (limited to 'src/Util/NumTheoryUtil.v')
-rw-r--r-- | src/Util/NumTheoryUtil.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 29fedaa9b..8b8595bb7 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -95,13 +95,13 @@ Proof. apply in_mod_ZPGroup; auto. Qed. -Lemma fermat_inv : forall a, a mod p <> 0 -> (a * (a^(p-2) mod p)) mod p = 1. +Lemma fermat_inv : forall a, a mod p <> 0 -> ((a^(p-2) mod p) * a) mod p = 1. Proof. intros. pose proof (prime_ge_2 _ prime_p). - rewrite Zmult_mod_idemp_r. - replace (a * a ^ (p - 2)) with (a^(p-1)). - 2:replace (a * a ^ (p - 2)) with (a^1 * a ^ (p - 2)) by ring. + rewrite Zmult_mod_idemp_l. + replace (a ^ (p - 2) * a) with (a^(p-1)). + 2:replace (a ^ (p - 2) * a) with (a^1 * a ^ (p - 2)) by ring. 2:rewrite <-Zpower_exp; try f_equal; omega. auto using fermat_little. Qed. |