diff options
| author | thery | 2019-07-10 14:29:37 +0200 |
|---|---|---|
| committer | Assia Mahboubi | 2019-09-16 10:21:09 +0200 |
| commit | fe30314bc728339353a9a4e490c8aedc61287752 (patch) | |
| tree | 7822138dd9fc4b0769961dc75f8e3418ca3fcf02 | |
| parent | ba669012734dc17a1050b49121009d083f346303 (diff) | |
fermat little theorem
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 15 |
2 files changed, 17 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 55f44e6..ba58cb3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -18,6 +18,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - Added theorem `totient_prime` in `prime.v` +- Added theorems `prime_modn_expSn` and `fermat_little` in `binomial.v` + ### Changed - `eqVneq` lemma is changed from `{x = y} + {x != y}` to diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 06774ff..5896858 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -333,6 +333,21 @@ Proof. by apply/eqP; elim/big_rec2: _ => // i m n _; rewrite modnDml eqn_modDl. Qed. +Lemma prime_modn_expSn p n : prime p -> n.+1 ^ p = (n ^ p).+1 %[mod p]. +Proof. +case: p => // p pP. +rewrite -[(_ ^ _).+1]addn0 (expnDn 1) big_ord_recr big_ord_recl /=. +rewrite subnn binn exp1n !mul1n addnAC -modnDmr; congr ((_ + _) %% _). +apply/eqP/dvdn_sum => -[i ?] _; exact/dvdn_mulr/prime_dvd_bin. +Qed. + +Lemma fermat_little a p : prime p -> a ^ p = a %[mod p]. +Proof. +move=> pP. +elim: a => [|a IH]; first by rewrite exp0n // prime_gt0. +by rewrite prime_modn_expSn // -addn1 -modnDml IH modnDml addn1. +Qed. + (* Combinatorial characterizations. *) Section Combinations. |