diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 7d07293..9eafea9 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -411,14 +411,21 @@ move=> pr_p pr_q; apply: negb_inj. by rewrite eqn_dvd negb_and -!prime_coprime // coprime_sym orbb. Qed. +Lemma Euclid_dvd1 p : prime p -> (p %| 1) = false. +Proof. by rewrite dvdn1; case: eqP => // ->. Qed. + Lemma Euclid_dvdM m n p : prime p -> (p %| m * n) = (p %| m) || (p %| n). Proof. move=> pr_p; case dv_pm: (p %| m); first exact: dvdn_mulr. by rewrite Gauss_dvdr // prime_coprime // dv_pm. Qed. -Lemma Euclid_dvd1 p : prime p -> (p %| 1) = false. -Proof. by rewrite dvdn1; case: eqP => // ->. Qed. +Lemma Euclid_dvd_prod (I : Type) (r : seq I) (P : pred I) (f : I -> nat) p : + prime p -> + p %| \prod_(i <- r | P i) f i = \big[orb/false]_(i <- r | P i) (p %| f i). +Proof. +move=> pP; apply: big_morph=> [x y|]; [exact: Euclid_dvdM | exact: Euclid_dvd1]. +Qed. Lemma Euclid_dvdX m n p : prime p -> (p %| m ^ n) = (p %| m) && (n > 0). Proof. |