diff options
| author | Laurent Théry | 2019-09-30 09:27:14 +0200 |
|---|---|---|
| committer | Assia Mahboubi | 2019-09-30 09:27:14 +0200 |
| commit | 020c051359aa05d1e22259b4739b9130ab65e472 (patch) | |
| tree | 3d70e7d4689e50d79b98b62e724adefb97b02bce | |
| parent | d3dc7c337f2f031cec57d1f8804d59662e36ecfb (diff) | |
ffact as a product similar to fact_prod (#374)
Thanks!
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 3 | ||||
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 7 |
2 files changed, 9 insertions, 1 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ba58cb3..5964257 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -18,7 +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` +- Added theorems `ffact_prod`,`prime_modn_expSn` and `fermat_little` + in `binomial.v` ### Changed diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 5896858..0c5be52 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -148,6 +148,13 @@ elim: n m => [|n IHn] [|m] //=; first by rewrite ffactn1 mul1n. by rewrite !ffactSS IHn mulnA. Qed. +Lemma ffact_prod n m : n ^_ m = \prod_(i < m) (n - i). +Proof. +elim: m n => [n | m IH [|n] //]; first by rewrite ffactn0 big_ord0. + by rewrite big_ord_recr /= sub0n muln0. +by rewrite ffactSS IH big_ord_recl subn0. +Qed. + Lemma ffact_gt0 n m : (0 < n ^_ m) = (m <= n). Proof. by elim: n m => [|n IHn] [|m] //=; rewrite ffactSS muln_gt0 IHn. Qed. |