diff options
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. *) |