diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-20 13:05:10 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-02-26 14:26:37 -0500 |
| commit | 01f66dcd54921fd973a6ef00706eb41130eb47e5 (patch) | |
| tree | b337d997468f7736687a765a20e484e75fa5b542 /src/Util/NumTheoryUtil.v | |
| parent | 9c129000ea8bce2c794af6179524f42d88a330a1 (diff) | |
ModularArithmetic: reasonable-time FieldToZ inv implementation
Diffstat (limited to 'src/Util/NumTheoryUtil.v')
| -rw-r--r-- | src/Util/NumTheoryUtil.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index eee651bc9..190fd5274 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -94,6 +94,17 @@ 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. +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 with (a^1) at 2 by ring. + 2:rewrite <-Zpower_exp; try f_equal; omega. + auto using fermat_little. +Qed. + Lemma squared_fermat_little: forall a (a_nonzero : a mod p <> 0), (a * a) ^ x mod p = 1. Proof. |