diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-05-24 14:09:47 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-05-24 14:09:47 -0400 |
commit | b9e60f74ff9378126a62cbe8f0981fc99c3dfca7 (patch) | |
tree | 587c27049bbaff49a0ca484500452f59f30f1832 /src/ModularArithmetic/PrimeFieldTheorems.v | |
parent | 6a59acc27e725056587d48e0e8393f0bf9850d74 (diff) |
PrimeFieldTheorems fermat inverse lemma: prove admit
Diffstat (limited to 'src/ModularArithmetic/PrimeFieldTheorems.v')
-rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 2bde727c8..70a2c4a87 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -184,7 +184,7 @@ Section VariousModPrime. intros. erewrite (Fq_inv_unique inv_fermat); trivial; split; intros; unfold inv_fermat. { replace 2%N with (Z.to_N (Z.of_N 2))%N by auto. - rewrite Fq_pow_zero. admit. intro. + rewrite Fq_pow_zero. reflexivity. intro. assert (Z.of_N (Z.to_N (q-2)) = 0%Z) by (rewrite H0; eauto); rewrite Z2N.id in *; omega. } { clear x. rename x0 into x. pose proof (fermat_inv _ _ x) as Hf; forward Hf. { pose proof @ZToField_FieldToZ; pose proof @ZToField_mod; congruence. } |