diff options
Diffstat (limited to 'src/Galois/GaloisTheory.v')
| -rw-r--r-- | src/Galois/GaloisTheory.v | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/src/Galois/GaloisTheory.v b/src/Galois/GaloisTheory.v index f8d1c4c7a..3cfa0323c 100644 --- a/src/Galois/GaloisTheory.v +++ b/src/Galois/GaloisTheory.v @@ -182,21 +182,31 @@ Module GaloisTheory (M: Modulus). Lemma inject_distr_add : forall (m n : Z), inject (m + n) = inject m + inject n. - Admitted. + Proof. + galois. + Qed. Lemma inject_distr_sub : forall (m n : Z), inject (m - n) = inject m - inject n. - Admitted. + Proof. + galois. + Qed. Lemma inject_distr_mul : forall (m n : Z), inject (m * n) = inject m * inject n. - Admitted. + Proof. + galois. + Qed. Lemma inject_eq : forall (x : GF), inject x = x. - Admitted. + Proof. + galois. + Qed. Lemma inject_mod_eq : forall x, inject x = inject (x mod modulus). - Admitted. + Proof. + galois. + Qed. Definition GFquotrem(a b: GF): GF * GF := match (Z.quotrem a b) with |