From b0293a7fef2ed784f30fb81dcd8c835f435d71eb Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 28 Feb 2016 20:09:51 -0500 Subject: Instance Fq_Integral_domain : @Integral_domain (F q) ... --- src/ModularArithmetic/PrimeFieldTheorems.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'src') 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. -- cgit v1.2.3