From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.ssreflect.binomial.html | 133 +++++++++++++-------------
1 file changed, 65 insertions(+), 68 deletions(-)
(limited to 'docs/htmldoc/mathcomp.ssreflect.binomial.html')
diff --git a/docs/htmldoc/mathcomp.ssreflect.binomial.html b/docs/htmldoc/mathcomp.ssreflect.binomial.html
index 085a24d..b6be0dc 100644
--- a/docs/htmldoc/mathcomp.ssreflect.binomial.html
+++ b/docs/htmldoc/mathcomp.ssreflect.binomial.html
@@ -21,7 +21,6 @@
@@ -53,16 +52,16 @@
@@ -73,50 +72,50 @@
@@ -129,44 +128,44 @@
Fixpoint binomial_rec n m :=
match n, m with
- | n'.+1, m'.+1 ⇒ binomial_rec n' m + binomial_rec n' m'
+ | n'.+1, m'.+1 ⇒ binomial_rec n' m + binomial_rec n' m'
| _, 0 ⇒ 1
- | 0, _.+1 ⇒ 0
+ | 0, _.+1 ⇒ 0
end.
-Definition binomial := nosimpl binomial_rec.
+Definition binomial := nosimpl binomial_rec.
-Notation "''C' ( n , m )" := (binomial n m)
+Notation "''C' ( n , m )" := (binomial n m)
(at level 8, format "''C' ( n , m )") : nat_scope.
-Lemma binE : binomial = binomial_rec.
+Lemma binE : binomial = binomial_rec.
-Lemma bin0 n : 'C(n, 0) = 1.
+Lemma bin0 n : 'C(n, 0) = 1.
-Lemma bin0n m : 'C(0, m) = (m == 0).
+Lemma bin0n m : 'C(0, m) = (m == 0).
-Lemma binS n m : 'C(n.+1, m.+1) = 'C(n, m.+1) + 'C(n, m).
+Lemma binS n m : 'C(n.+1, m.+1) = 'C(n, m.+1) + 'C(n, m).
-Lemma bin1 n : 'C(n, 1) = n.
+Lemma bin1 n : 'C(n, 1) = n.
-Lemma bin_gt0 n m : (0 < 'C(n, m)) = (m ≤ n).
+Lemma bin_gt0 n m : (0 < 'C(n, m)) = (m ≤ n).
-Lemma leq_bin2l n1 n2 m : n1 ≤ n2 → 'C(n1, m) ≤ 'C(n2, m).
+Lemma leq_bin2l n1 n2 m : n1 ≤ n2 → 'C(n1, m) ≤ 'C(n2, m).
-Lemma bin_small n m : n < m → 'C(n, m) = 0.
+Lemma bin_small n m : n < m → 'C(n, m) = 0.
-Lemma binn n : 'C(n, n) = 1.
+Lemma binn n : 'C(n, n) = 1.
@@ -175,10 +174,10 @@
Multiply to move diagonally down and right in the Pascal triangle.
@@ -187,16 +186,16 @@
In fact the only exception for bin_factd is n = 0 and m = 1
-
Lemma bin_factd n m : 0
< n → 'C(n, m) = n`! %/ (m`! × (n - m)`!).
+
Lemma bin_factd n m : 0
< n → 'C(n, m) = n`! %/ (m`! × (n - m)`!).
-
Lemma bin_ffact n m :
'C(n, m) × m`! = n ^_ m.
+
Lemma bin_ffact n m :
'C(n, m) × m`! = n ^_ m.
-
Lemma bin_ffactd n m :
'C(n, m) = n ^_ m %/ m`!.
+
Lemma bin_ffactd n m :
'C(n, m) = n ^_ m %/ m`!.
-
Lemma bin_sub n m :
m ≤ n → 'C(n, n - m) = 'C(n, m).
+
Lemma bin_sub n m :
m ≤ n → 'C(n, n - m) = 'C(n, m).
-
Lemma mul_bin_left n m :
m.+1 × 'C(n, m.+1) = (n - m) × 'C(n, m).
+
Lemma mul_bin_left n m :
m.+1 × 'C(n, m.+1) = (n - m) × 'C(n, m).
-
Lemma binSn n :
'C(n.+1, n) = n.+1.
+
Lemma binSn n :
'C(n.+1, n) = n.+1.
-
Lemma bin2 n :
'C(n, 2
) = (n × n.-1)./2.
+
Lemma bin2 n :
'C(n, 2
) = (n × n.-1)./2.
-
Lemma bin2odd n :
odd n → 'C(n, 2
) = n × n.-1./2.
+
Lemma bin2odd n :
odd n → 'C(n, 2
) = n × n.-1./2.
-
Lemma prime_dvd_bin k p :
prime p → 0
< k < p → p %| 'C(p, k).
+
Lemma prime_dvd_bin k p :
prime p → 0
< k < p → p %| 'C(p, k).
-
Lemma triangular_sum n :
\sum_(0
≤ i < n) i = 'C(n, 2
).
+
Lemma triangular_sum n :
\sum_(0
≤ i < n) i = 'C(n, 2
).
-
Lemma textbook_triangular_sum n :
\sum_(0
≤ i < n) i = 'C(n, 2
).
+
Lemma textbook_triangular_sum n :
\sum_(0
≤ i < n) i = 'C(n, 2
).
Theorem Pascal a b n :
-
(a + b) ^ n = \sum_(i < n.+1) 'C(n, i) × (a ^ (n - i) × b ^ i).
+
(a + b) ^ n = \sum_(i < n.+1) 'C(n, i) × (a ^ (n - i) × b ^ i).
Definition expnDn :=
Pascal.
Lemma Vandermonde k l i :
-
\sum_(j < i.+1) 'C(k, j) × 'C(l, i - j) = 'C(k + l , i).
+
\sum_(j < i.+1) 'C(k, j) × 'C(l, i - j) = 'C(k + l , i).
Lemma subn_exp m n k :
-
m ^ k - n ^ k = (m - n) × (\sum_(i < k) m ^ (k.-1 -i) × n ^ i).
+
m ^ k - n ^ k = (m - n) × (\sum_(i < k) m ^ (k.-1 -i) × n ^ i).
-
Lemma predn_exp m k :
(m ^ k).-1 = m.-1 × (\sum_(i < k) m ^ i).
+
Lemma predn_exp m k :
(m ^ k).-1 = m.-1 × (\sum_(i < k) m ^ i).
-
Lemma dvdn_pred_predX n e : (
n.-1 %| (n ^ e).-1)%
N.
+
Lemma dvdn_pred_predX n e : (
n.-1 %| (n ^ e).-1)%
N.
-
Lemma modn_summ I r (
P :
pred I)
F d :
-
\sum_(i <- r | P i) F i %% d = \sum_(i <- r | P i) F i %[mod d].
+
Lemma modn_summ I r (
P :
pred I)
F d :
+
\sum_(i <- r | P i) F i %% d = \sum_(i <- r | P i) F i %[mod d].
-Lemma card_uniq_tuples T n (A : pred T) :
- #|[set t : n.-tuple T | all A t & uniq t]| = #|A| ^_ n.
+Lemma card_uniq_tuples T n (A : pred T) :
+ #|[set t : n.-tuple T | all A t & uniq t]| = #|A| ^_ n.
-Lemma card_inj_ffuns_on D T (R : pred T) :
- #|[set f : {ffun D → T} in ffun_on R | injectiveb f]| = #|R| ^_ #|D|.
+Lemma card_inj_ffuns_on D T (R : pred T) :
+ #|[set f : {ffun D → T} in ffun_on R | injectiveb f]| = #|R| ^_ #|D|.
Lemma card_inj_ffuns D T :
- #|[set f : {ffun D → T} | injectiveb f]| = #|T| ^_ #|D|.
+ #|[set f : {ffun D → T} | injectiveb f]| = #|T| ^_ #|D|.
-Lemma cards_draws T (B : {set T}) k :
- #|[set A : {set T} | A \subset B & #|A| == k]| = 'C(#|B|, k).
+Lemma cards_draws T (B : {set T}) k :
+ #|[set A : {set T} | A \subset B & #|A| == k]| = 'C(#|B|, k).
-Lemma card_draws T k : #|[set A : {set T} | #|A| == k]| = 'C(#|T|, k).
+Lemma card_draws T k : #|[set A : {set T} | #|A| == k]| = 'C(#|T|, k).
Lemma card_ltn_sorted_tuples m n :
- #|[set t : m.-tuple 'I_n | sorted ltn (map val t)]| = 'C(n, m).
+ #|[set t : m.-tuple 'I_n | sorted ltn (map val t)]| = 'C(n, m).
Lemma card_sorted_tuples m n :
- #|[set t : m.-tuple 'I_n.+1 | sorted leq (map val t)]| = 'C(m + n, m).
+ #|[set t : m.-tuple 'I_n.+1 | sorted leq (map val t)]| = 'C(m + n, m).
Lemma card_partial_ord_partitions m n :
- #|[set t : m.-tuple 'I_n.+1 | \sum_(i <- t) i ≤ n]| = 'C(m + n, m).
+ #|[set t : m.-tuple 'I_n.+1 | \sum_(i <- t) i ≤ n]| = 'C(m + n, m).
Lemma card_ord_partitions m n :
- #|[set t : m.+1.-tuple 'I_n.+1 | \sum_(i <- t) i == n]| = 'C(m + n, m).
+ #|[set t : m.+1.-tuple 'I_n.+1 | \sum_(i <- t) i == n]| = 'C(m + n, m).
End Combinations.
-
-
--
cgit v1.2.3