diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-10 15:10:34 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-10 15:10:34 -0400 |
| commit | 1d3a90c2fb96ad5704718e9c0eb214ca177b04f8 (patch) | |
| tree | 79b9d4e6e6935c4d7213f7185da35ed3e9dd9c0c /src/Util/ZUtil/Modulo.v | |
| parent | 6ee6d5242d8caab769bd60ee4d44efe41add8bda (diff) | |
Rename power_mod_full to mod_pow_full for similarity with std lib
Diffstat (limited to 'src/Util/ZUtil/Modulo.v')
| -rw-r--r-- | src/Util/ZUtil/Modulo.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v index 2146d119f..f4405bef3 100644 --- a/src/Util/ZUtil/Modulo.v +++ b/src/Util/ZUtil/Modulo.v @@ -149,7 +149,7 @@ Module Z. Qed. Hint Rewrite mod_div_eq0 using zutil_arith : zsimplify. - Lemma power_mod_full p q n : (p^q) mod n = ((p mod n)^q) mod n. + Lemma mod_pow_full p q n : (p^q) mod n = ((p mod n)^q) mod n. Proof. destruct (Z_dec' n 0) as [ [H|H] | H]; subst; [ |