diff options
| -rw-r--r-- | mathcomp/algebra/poly.v | 7 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 2 |
2 files changed, 3 insertions, 6 deletions
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 1c5de11..5019eda 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -1950,10 +1950,7 @@ Qed. Lemma coef_comp_poly p q n : (p \Po q)`_n = \sum_(i < size p) p`_i * (q ^+ i)`_n. -Proof. -rewrite comp_polyE coef_sum. -by elim/big_ind2: _ => [//|? ? ? ? -> -> //|i]; rewrite coefZ. -Qed. +Proof. by rewrite comp_polyE coef_sum; apply: eq_bigr => i; rewrite coefZ. Qed. Lemma polyOver_comp S (ringS : semiringPred S) (kS : keyed_pred ringS) : {in polyOver kS &, forall p q, p \Po q \in polyOver kS}. @@ -2255,7 +2252,7 @@ rewrite big_split /= addnK -big_andE /=. by elim/big_ind2: _ => // [[] [|n] [] [|m]|i Pi]; rewrite -?polySpred ?F_neq0. Qed. -Lemma size_prod_seq_eq1 (I : choiceType) (s : seq I) (F : I -> {poly R}) : +Lemma size_prod_seq_eq1 (I : eqType) (s : seq I) (F : I -> {poly R}) : reflect (forall i, i \in s -> size (F i) = 1%N) (size (\prod_(i <- s) F i) == 1%N). Proof. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 31579ce..9ccb92f 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -1172,7 +1172,7 @@ Lemma signrMK n : @involutive R ( *%R ((-1) ^+ n)). Proof. by move=> x; rewrite mulrA -expr2 sqrr_sign mul1r. Qed. Lemma lastr_eq0 (s : seq R) x : x != 0 -> (last x s == 0) = (last 1 s == 0). -Proof. by elim: s => [|y s ihs] /negPf // ->; rewrite oner_eq0. Qed. +Proof. by case: s => [|y s] /negPf // ->; rewrite oner_eq0. Qed. Lemma mulrI_eq0 x y : lreg x -> (x * y == 0) = (y == 0). Proof. by move=> reg_x; rewrite -{1}(mulr0 x) (inj_eq reg_x). Qed. |