diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-17 08:59:10 -0500 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:40:31 -0400 |
| commit | e907b22802825e9ff102e284b8f4b9ddd119fdca (patch) | |
| tree | e2a50503b6ce23629f0c4ef35b22bbf8ab5cf4b6 /src | |
| parent | 17cf6fb43ea9ddda03cfa1071db5b0dd9a617e25 (diff) | |
update ModularArithmetic tutorial
Diffstat (limited to 'src')
| -rw-r--r-- | src/ModularArithmetic/Tutorial.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v index cabb8501b..425816f9e 100644 --- a/src/ModularArithmetic/Tutorial.v +++ b/src/ModularArithmetic/Tutorial.v @@ -23,7 +23,7 @@ Section Mod24. div (@Fmorph_div_theory q), power_tac (@Fpower_theory q) [Fexp_tac]). - Lemma sumOfSquares : forall a b: F q, (a+b)^2 = a^2 + ZToField 2*a*b + b^2. + Lemma sumOfSquares : forall a b: F q, (a+b)^2 = a^2 + 2*a*b + b^2. Proof. intros. ring. @@ -51,7 +51,7 @@ Section Modq. div (@Fmorph_div_theory q), power_tac (@Fpower_theory q) [Fexp_tac]). - Lemma sumOfSquares' : forall a b: F q, (a+b)^2 = a^2 + ZToField 2*a*b + b^2. + Lemma sumOfSquares' : forall a b c: F q, c <> 0 -> ((a+b)/c)^2 = a^2/c^2 + ZToField 2*(a/c)*(b/c) + b^2/c^2. Proof. intros. field. |