diff options
| author | Cyril Cohen | 2019-11-27 18:47:27 +0100 |
|---|---|---|
| committer | GitHub | 2019-11-27 18:47:27 +0100 |
| commit | cbc1688d9447860a60cb3ede83099a10bcd408e2 (patch) | |
| tree | 2471481f9a004a03d5b96c28ebaf1ee7e2f06e19 /mathcomp/algebra/poly.v | |
| parent | 8b78152ce646d0f2f91b7c90f204dd98ef6a1d4b (diff) | |
| parent | 4bd5ba38e4f6c6456a8fcc39364a67b51fde92f2 (diff) | |
Merge pull request #441 from ggonthier/big_enum
Big enum
Diffstat (limited to 'mathcomp/algebra/poly.v')
| -rw-r--r-- | mathcomp/algebra/poly.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 2bb3614..25037e8 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -922,7 +922,10 @@ by rewrite size_XsubC. Qed. Lemma size_exp_XsubC n a : size (('X - a%:P) ^+ n) = n.+1. -Proof. by rewrite -[n]card_ord -prodr_const size_prod_XsubC cardE enumT. Qed. +Proof. +rewrite -[n]card_ord -prodr_const -big_filter size_prod_XsubC. +by have [e _ _ [_ ->]] := big_enumP. +Qed. (* Some facts about regular elements. *) |