diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-07-28 22:30:02 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-08-04 11:47:51 -0400 |
| commit | 333f867f010eb00db777916d4ee757f9ff2216b4 (patch) | |
| tree | d0eac47f90b1e04f51c9c135875eaaef28f9497b /src | |
| parent | 4964f1ff2d40ba08573deddca56140c4ac4b19eb (diff) | |
prove an admit
Diffstat (limited to 'src')
| -rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index c97bde495..e0c778456 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -71,8 +71,9 @@ Module Zmod. Lemma Fq_inv_fermat (x:F q) : inv x = x ^ Z.to_N (q - 2)%Z. Proof. - destruct (dec (x = 0%F)) as [?|Hnz]; [subst x; rewrite inv_0|]. - { admit. } + destruct (dec (x = 0%F)) as [?|Hnz]. + { subst x; rewrite inv_0, pow_0_l; trivial. + change (0%N) with (Z.to_N 0%Z); rewrite Z2N.inj_iff; omega. } erewrite <-Algebra.Field.inv_unique; try reflexivity. rewrite eq_FieldToZ_iff, FieldToZ_mul, FieldToZ_pow, Z2N.id, FieldToZ_1 by omega. apply (fermat_inv q _ (FieldToZ x)); rewrite mod_FieldToZ; eapply FieldToZ_nonzero; trivial. |