diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-01-13 12:20:35 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2016-01-13 12:20:35 -0500 |
| commit | 088a1b2bd7ba87d74aa3b5308df04cb16e14d0cd (patch) | |
| tree | 0ebb00d9b3d13036908dab1f9b2a725ce66173d6 /src/Scratch/fermat.v | |
| parent | 97cd9a342824b3d6ceac707ca1aab5e552075b3f (diff) | |
| parent | f4425e8a1de9cff978f794e4783eff1bcfede412 (diff) | |
Merge branch 'master' of github.mit.edu:plv/fiat-crypto
Diffstat (limited to 'src/Scratch/fermat.v')
| -rw-r--r-- | src/Scratch/fermat.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Scratch/fermat.v b/src/Scratch/fermat.v index 7871db92f..947ffce15 100644 --- a/src/Scratch/fermat.v +++ b/src/Scratch/fermat.v @@ -42,7 +42,7 @@ Section Fq. Axiom inv : Fq -> Fq. Axiom inv_spec : forall a, inv a * a = one. - Definition div a b := add a (inv b). + Definition div a b := mul a (inv b). Infix "/" := div. Fixpoint replicate {T} n (x:T) : list T := match n with O => nil | S n' => x::replicate n' x end. |