diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 11 |
2 files changed, 10 insertions, 3 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5964257..43bc379 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -16,7 +16,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - Added functions `tuple_of_finfun`, `finfun_of_tuple`, and their "cancellation" lemmas. -- Added theorem `totient_prime` in `prime.v` +- Added theorems `totient_prime` `Euclid_dvd_prod` in `prime.v` - Added theorems `ffact_prod`,`prime_modn_expSn` and `fermat_little` in `binomial.v` 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. |