diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-02-28 20:09:51 -0500 |
---|---|---|
committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:42:16 -0400 |
commit | b0293a7fef2ed784f30fb81dcd8c835f435d71eb (patch) | |
tree | f87f0b469a2eb82f76f6d3b177fad3aae8cf0fd5 /src | |
parent | 8f77ab8ace0f63beedff8588c4bf79d502b3107d (diff) |
Instance Fq_Integral_domain : @Integral_domain (F q) ...
Diffstat (limited to 'src')
-rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 440d30552..2e778dc5f 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -1,6 +1,7 @@ Require Export Spec.ModularArithmetic ModularArithmetic.ModularArithmeticTheorems. Require Export Ring_theory Field_theory Field_tac. +Require Import Nsatz. Require Import Crypto.ModularArithmetic.Pre. Require Import Util.NumTheoryUtil. Require Import Tactics.VerdiTactics. @@ -322,6 +323,25 @@ Section VariousModPrime. rewrite <- z_2x_0 in opp_spec. apply F_add_reg_l in opp_spec; auto. Qed. + + Instance Fq_Ring_ops : @Ring_ops (F q) 0 1 add mul sub opp eq. + Instance Fq_Ring: @Ring (F q) 0 1 add mul sub opp eq Fq_Ring_ops. + Proof. + econstructor; eauto with typeclass_instances; + unfold R2, equality, eq_notation, addition, add_notation, one, one_notation, + multiplication, mul_notation, zero, zero_notation, subtraction, + sub_notation, opposite, opp_notation; intros; ring. + Qed. + + Instance Fq_Cring: @Cring (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring. + Proof. + repeat intro. apply F_mul_comm. + Qed. + + Instance Fq_Integral_domain : @Integral_domain (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring Fq_Cring. + Proof. + econstructor; eauto using Fq_mul_zero_why, Fq_1_neq_0. + Qed. End VariousModPrime. Section SquareRootsPrime5Mod8. |