diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-17 19:10:54 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-02-17 19:10:54 -0500 |
| commit | a46dbbec5fc2cd3ffc5c6d4be751e42aa2b7cafb (patch) | |
| tree | 24576fec124d612be19cdca16dcc799250e2a7fa /src/ModularArithmetic/PrimeFieldTheorems.v | |
| parent | 56fa6655b07e8992677805e4f89e131c221755a6 (diff) | |
efficient powmod
Diffstat (limited to 'src/ModularArithmetic/PrimeFieldTheorems.v')
| -rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 2cc494224..a49138c86 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -227,13 +227,13 @@ Section VariousModPrime. + pose proof (FieldToZ_nonzero_range a a_nonzero); omega. + replace (q / 2)%Z with (Z.of_N (Z.to_N (q / 2))) by (apply Z2N.id; apply Z.div_pos; prime_bound). - rewrite FieldToZ_pow by omega. + rewrite FieldToZ_pow_Zpow_mod by omega. rewrite A. replace (FieldToZ 1) with (1 mod q) by auto. apply Z.mod_1_l; omega. } { apply F_eq. - rewrite <- FieldToZ_pow by omega. + rewrite <- FieldToZ_pow_Zpow_mod by omega. rewrite Z2N.id by (apply Z.div_pos; omega). replace (FieldToZ 1) with 1%Z by (rewrite FieldToZ_ZToField at 1; symmetry; apply Zmod_1_l; omega). @@ -367,4 +367,4 @@ Section SquareRootsPrime5Mod8. field. Qed. -End SquareRootsPrime5Mod8. +End SquareRootsPrime5Mod8.
\ No newline at end of file |