val irred_poly (f: G.field) : poly
let irred_poly (f:G.field) : poly =
  let G.GF t irred = f in
  monomial (I.bits t) +. to_poly #f irred
val irred_poly (f: G.field) : poly
let irred_poly (f: G.field) : poly =
let G.GF t irred = f in
monomial (I.bits t) +. to_poly #f irred
Vale.Math.Poly2.Galois.fsti.checked
Vale.Math.Poly2_s.fsti.checked Vale.Math.Poly2.fsti.checked Spec.GaloisField.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked
Vale.Math.Poly2.Galois.fsti
Spec.GaloisField.field Lib.IntTypes.inttype Prims.l_and Prims.b2t Lib.IntTypes.unsigned Prims.op_disEquality Lib.IntTypes.U1 Lib.IntTypes.uint_t Lib.IntTypes.SEC Vale.Math.Poly2.op_Plus_Dot Vale.Math.Poly2_s.monomial Lib.IntTypes.bits Vale.Math.Poly2.Galois.to_poly Vale.Math.Poly2_s.poly
module Vale.Math.Poly2.Galois
open FStar.Mul
module I = Lib.IntTypes
module G = Spec.GaloisField
module P = Vale.Math.Poly2_s
open Vale.Math.Poly2_s
open Vale.Math.Poly2
open FStar.Seq

(*
Connect Spec.GaloisField to Vale.Math.Poly2*
*)

val to_poly (#f:G.field) (e:G.felem f) : poly
val to_felem (f:G.field) (p:poly) : G.felem f
val irred_poly (f: G.field) : poly
f: Spec.GaloisField.field -> Vale.Math.Poly2_s.poly