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