blob: a196c7bf81a3d36db5889ac1ebeb3df6ce374179 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Require Import BinInt BinNat ZArith Znumtheory.
Require Import Eqdep_dec.
Require Import Tactics.VerdiTactics.
Require Import Galois GaloisTheory.
Module AbstractGaloisField (M: Modulus).
Module G := Galois M.
Module T := GaloisTheory M.
Export M G T.
Add Field GFfield_computational : GFfield_theory
(completeness GFcomplete,
div GFdiv_theory,
power_tac GFpower_theory [GFexp_tac]).
End AbstractGaloisField.
|
