diff options
Diffstat (limited to 'mathcomp/algebra/zmodp.v')
| -rw-r--r-- | mathcomp/algebra/zmodp.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v index 015d971..505fda9 100644 --- a/mathcomp/algebra/zmodp.v +++ b/mathcomp/algebra/zmodp.v @@ -142,7 +142,7 @@ Proof. by move=> Ux; rewrite /= Zp_mulC Zp_mulVz. Qed. Lemma Zp_intro_unit x y : Zp_mul y x = Zp1 -> coprime p x. Proof. case=> yx1; have:= coprimen1 p. -by rewrite -coprime_modr -yx1 coprime_modr coprime_mulr; case/andP. +by rewrite -coprime_modr -yx1 coprime_modr coprimeMr; case/andP. Qed. Lemma Zp_inv_out x : ~~ coprime p x -> Zp_inv x = x. |