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

Information

namegfp-thm
version1.52
descriptionProperties of GF(p) finite fields
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-11-10
requiresbool
gfp-def
gfp-witness
natural
natural-divides
natural-prime
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

x n. x n = 0 x = 0 ¬(n = 0)

Input Type Operators

Input Constants

Assumptions

odd oddprime

prime oddprime

¬odd 0

¬prime 1

¬(oddprime = 0)

¬

¬

bit0 0 = 0

t. t t

p. p

(¬) = λp. p

() = λp. p = λx.

t. t

t. t t

t. t t

t. t t t

x. fromNatural (toNatural x) = x

n. ¬(suc n = 0)

t. ( t) ¬t

n. bit1 n = suc (bit0 n)

n. ¬even n odd n

() = λp q. p q p

x. x 0 = 1

x. x * 0 = 0

x. 0 * x = 0

x. x * 1 = x

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

m. m = 0 n. m = suc n

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

() = λp. q. (x. p x q) q

x n. x suc n = x * x n

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)

p. p 0 (n. p n p (suc n)) n. p n

a. divides a 2 a = 1 a = 2

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