Skip to content

Instantly share code, notes, and snippets.

@methylene

methylene/prime_field.v

Last active March 27, 2016 20:16
Show Gist options
  • Save methylene/f362c0df81a8d6116656 to your computer and use it in GitHub Desktop.
Save methylene/f362c0df81a8d6116656 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
prime_field.v
Require Import ZArith.
Require Import Znumtheory.
Definition prime_z := {f | prime f}.
Record prime_field (f: prime_z) : Set := pf_make {n: Z}.
Definition pf_add {p: prime_z} (x y : (prime_field p)) :=
pf_make p ((n _ x) + (n _ y)).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment