blob: 23b1c8dd89f7ff6e567b13f983dc7f8da1e6183b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
Require Import BinInt BinNat ZArith Znumtheory.
Require Import BoolEq.
Require Import Galois GaloisTheory.
Module ZGaloisField (M: Modulus).
Module G := Galois M.
Module T := GaloisTheory M.
Export M G T.
Lemma GFring_morph:
ring_morph GFzero GFone GFplus GFmult GFminus GFopp eq
0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
inject.
Proof.
constructor; intros; try galois;
try (apply gf_eq; simpl; intuition).
apply Zmod_small; destruct modulus; simpl;
apply prime_ge_2 in p; intuition.
replace (- (x mod modulus)) with (0 - (x mod modulus));
try rewrite Zminus_mod_idemp_r; trivial.
replace x with y; intuition.
symmetry; apply Zeq_bool_eq; trivial.
Qed.
Add Ring GFring_Z : GFring_theory
(morphism GFring_morph,
power_tac GFpower_theory [GFexp_tac]).
Add Field GFfield_Z : GFfield_theory
(morphism GFring_morph,
power_tac GFpower_theory [GFexp_tac]).
End ZGaloisField.
|
