diff options
Diffstat (limited to 'src/ModularArithmetic')
-rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 3 | ||||
-rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 6 |
2 files changed, 5 insertions, 4 deletions
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 44b422767..262b20e3e 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -6,7 +6,8 @@ Require Import Coq.ZArith.BinInt Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArit Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac. -Require Import Crypto.Algebra Crypto.Util.Decidable Crypto.Util.ZUtil. +Require Import Crypto.Algebra Crypto.Algebra.Ring Crypto.Algebra.Field. +Require Import Crypto.Util.Decidable Crypto.Util.ZUtil. Require Export Crypto.Util.FixCoqMistakes. Module F. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index e0dfc8f1a..abc30056f 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -12,7 +12,7 @@ Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Decidable. Require Export Crypto.Util.FixCoqMistakes. -Require Crypto.Algebra. +Require Crypto.Algebra Crypto.Algebra.Field. Existing Class prime. @@ -226,7 +226,7 @@ Module F. split; try apply eq_b4_a2. intro Hyy. rewrite !@F.pow_2_r in *. - destruct (Algebra.only_two_square_roots_choice _ x (x * x) Hyy eq_refl); clear Hyy; + destruct (Field.only_two_square_roots_choice _ x (x * x) Hyy eq_refl); clear Hyy; [ eexists; eassumption | ]. match goal with H : ?a * ?a = F.opp _ |- _ => exists (sqrt_minus1 * a); rewrite mul_square_sqrt_minus1; rewrite H end. @@ -254,7 +254,7 @@ Module F. break_if. intuition (f_equal; eauto). split; intro A. { - destruct (Algebra.only_two_square_roots_choice _ x (x * x) A eq_refl) as [B | B]; + destruct (Field.only_two_square_roots_choice _ x (x * x) A eq_refl) as [B | B]; clear A; try congruence. rewrite mul_square_sqrt_minus1, B; field. } { |