diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-17 08:59:10 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-02-17 08:59:10 -0500 |
| commit | 56fa6655b07e8992677805e4f89e131c221755a6 (patch) | |
| tree | c36e808f1218f8c52e95b3a2c14f86e85c6c5e85 /src/ModularArithmetic | |
| parent | b551159160caf12cea50ef765cc2fdd0d4ed096d (diff) | |
update ModularArithmetic tutorial
Diffstat (limited to 'src/ModularArithmetic')
| -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. |