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 | |
| parent | 6ee6d5242d8caab769bd60ee4d44efe41add8bda (diff) | |
Rename power_mod_full to mod_pow_full for similarity with std lib
Diffstat (limited to 'src/Util/ZUtil')
| -rw-r--r-- | src/Util/ZUtil/EquivModulo.v | 2 | ||||
| -rw-r--r-- | src/Util/ZUtil/Modulo.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/ZUtil/EquivModulo.v b/src/Util/ZUtil/EquivModulo.v index 3578a8223..586d16828 100644 --- a/src/Util/ZUtil/EquivModulo.v +++ b/src/Util/ZUtil/EquivModulo.v @@ -32,7 +32,7 @@ Module Z. Local Instance pow_mod_Proper : Proper (equiv_modulo ==> eq ==> equiv_modulo) Z.pow. Proof. intros ?? H ???; subst; hnf in H |- *. - rewrite Z.power_mod_full, H, <- Z.power_mod_full; reflexivity. + rewrite Z.mod_pow_full, H, <- Z.power_mod_full; reflexivity. Qed. Local Instance modulo_equiv_modulo_Proper 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; [ |