Package gfp-thm: Properties of GF(p) finite fields

Information

namegfp-thm
version1.14
descriptionProperties of GF(p) finite fields
authorJoe Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-02-10
requiresbool
natural
natural-divides
natural-prime
gfp-witness
gfp-def
showData.Bool
Number.GF(p)
Number.Natural

Files

Theorems

1 < oddprime

¬(oddprime = 1)

¬divides oddprime 1

2 < oddprime

¬(oddprime = 2)

¬divides oddprime 2

¬divides 2 oddprime

¬(1 = 0)

1 mod oddprime = 1

¬(2 = 0)

2 mod oddprime = 2

m n. divides oddprime (m * n) divides oddprime m divides oddprime n

x y. x * y = 0 x = 0 y = 0

Input Type Operators

Input Constants

Assumptions

odd oddprime

prime oddprime

¬prime 1

¬(oddprime = 0)

¬

¬

odd 0

bit0 0 = 0

t. t t

p. p

(¬) = λp. p

() = λp. p = λx.

t. t t

t. t t

x. fromNatural (toNatural x) = x

n. bit1 n = suc (bit0 n)

n. ¬even n odd n

() = λp q. p q p

x. x * 0 = 0

x. 0 * x = 0

n. odd (suc n) ¬odd n

n. 0 < n ¬(n = 0)

n. bit0 (suc n) = suc (suc (bit0 n))

a. divides 2 a even a

n. n < oddprime n mod oddprime = n

a. divides a 1 a = 1

x. fromNatural x = 0 divides oddprime x

m n. suc m n m < n

() = λp q. (λf. f p q) = λf. f

x1 y1. fromNatural (x1 * y1) = fromNatural x1 * fromNatural y1

() = λp q. r. (p r) (q r) r

m n. m < n m n ¬(m = n)

a. divides a 2 a = 1 a = 2

p m n. prime p (divides p (m * n) divides p m divides p n)