Package gfp-div-thm: Properties of GF(p) field division

Information

namegfp-div-thm
version1.64
descriptionProperties of GF(p) field division
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2014-11-17
checksumcdcd2278ee5eca50bf0d4a159488bf0021c0008e
requiresbool
gfp-def
gfp-div-def
gfp-thm
natural
showData.Bool
Number.GF(p)
Number.Natural

Files

Theorems

inv 1 = 1

x. x / 1 = x

x. ¬(x = 0) inv (inv x) = x

x. ¬(x = 0) ¬(inv x = 0)

x. ¬(x = 0) x * inv x = 1

x y. ¬(x = 0) x * (y / x) = y

x y. ¬(x = 0) (y / x) * x = y

x y. ¬(x = 0) y * x / x = y

x y. ¬(x = 0) y / x = y * inv x

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

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

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

x. ¬(x = 0) inv x = 1 x = 1

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

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

x y. x * y = if y = 0 then 0 else x / (1 / y)

x y z. ¬(x = 0) x * y = x * z y = z

x y z. ¬(x = 0) y * x = z * x y = z

x y. ¬(x = 0) ¬(y = 0) ¬(y / x = 0)

x y. ¬(x = 0) ¬(y = 0) inv (y / x) = x / y

x y. ¬(x = 0) ¬(y = 0) inv x = inv y x = y

x y. ¬(x = 0) ¬(y = 0) inv x * inv y = inv (x * y)

x y z. ¬(y = 0) ¬(z = 0) x / (y / z) = x * z / y

External Type Operators

External Constants

Assumptions

¬

p. p

t. t ¬t

(¬) = λp. p

() = λp. p = λx.

t. t

t. t t

t. t t

t. t t

t. t

¬(1 = 0)

t. t ¬t

() = λp q. p q p

x. x 0 = 1

x. x * 0 = 0

x. 0 * x = 0

x. x * 1 = x

x. 1 * x = x

x y. x = y y = x

x y. x * y = y * x

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

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

x n. x suc n = x * x n

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

x y z. x = y y = z x = z

x y z. x * y * z = x * (y * z)

x. ¬(x = 0) inv x * x = 1

x y. ¬(x = 0) x * y / x = y

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

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

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

p c x y. p (if c then x else y) (c p x) (¬c p y)