|
name
|
gfp-def
|
|
version
|
1.76
|
|
requires
|
|
|
meta.description
|
Definition of GF(p) finite fields
|
|
meta.author
|
Joe Leslie-Hurd <joe@gilith.com>
|
|
meta.license
|
MIT
|
|
meta.provenance
|
HOL Light theory extracted on 2014-11-01
|
|
meta.show
|
"Data.Bool"
|
|
meta.show
|
"Number.GF(p)"
|
|
meta.show
|
"Number.Natural"
|
|
meta.show
|
"Probability.Random"
|
|
subs
|
2 subs
|
name
|
modular
|
|
imports
|
|
|
package
|
modular-1.92
|
|
interpretation
|
interpretation
-
type "Number.Modular.modular" as "Number.GF(p).gfp"
-
const "Number.Modular.*" as "Number.GF(p).*"
-
const "Number.Modular.+" as "Number.GF(p).+"
-
const "Number.Modular.-" as "Number.GF(p).-"
-
const "Number.Modular.<" as "Number.GF(p).<"
-
const "Number.Modular.<=" as "Number.GF(p).<="
-
const "Number.Modular.^" as "Number.GF(p).^"
-
const "Number.Modular.~" as "Number.GF(p).~"
-
const "Number.Modular.fromNatural" as "Number.GF(p).fromNatural"
-
const "Number.Modular.modulus" as "Number.GF(p).oddprime"
-
const "Number.Modular.random" as "Number.GF(p).random"
-
const "Number.Modular.toNatural" as "Number.GF(p).toNatural"
|
|