diff options
| author | Erik Martin-Dorel | 2019-02-27 17:31:35 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-03-20 12:54:26 +0100 |
| commit | c07f1f8d89dd1f975e06e8c45df2c7a4e6ca7fc3 (patch) | |
| tree | 73c109057bf3f18127be887fcc1b2e0ba82ff3e2 /mathcomp/algebra | |
| parent | 4c8455594c5adff08761037a5919c058d0d502ba (diff) | |
Add extra eta lemmas for the under tactic
Related: coq/coq#9651
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 5 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 4 |
2 files changed, 9 insertions, 0 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 3b12802..2580741 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -232,8 +232,13 @@ rewrite /fun_of_matrix; split=> [/= eqAB | -> //]. by apply/val_inj/ffunP=> [[i j]]; apply: eqAB. Qed. +Lemma eq_mx k F1 F2 : (F1 =2 F2) -> matrix_of_fun k F1 = matrix_of_fun k F2. +Proof. by move=> eq_F; apply/matrixP => i j; rewrite !mxE eq_F. Qed. + End MatrixDef. +Arguments eq_mx {R m n k} [F1] F2 eq_F12. + Bind Scope ring_scope with matrix. Notation "''M[' R ]_ ( m , n )" := (matrix R m n) (only parsing): type_scope. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 702dfc4..e0feecf 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -1673,6 +1673,9 @@ apply: eq_bigr => i _; case: leqP => // /nderivn_poly0->. by rewrite horner0 simp. Qed. +Lemma eq_poly n E1 E2 : E1 =1 E2 -> poly n E1 = poly n E2. +Proof. by move=> E; rewrite !poly_def; apply: eq_bigr => i _; rewrite E. Qed. + End PolynomialTheory. Prenex Implicits polyC polyCK Poly polyseqK lead_coef root horner polyOver. @@ -1695,6 +1698,7 @@ Arguments rootPt {R p x}. Arguments unity_rootP {R n z}. Arguments polyOverP {R S0 addS kS p}. Arguments polyC_inj {R} [x1 x2] eq_x12P. +Arguments eq_poly {R n} [E1] E2 eq_E12. Canonical polynomial_countZmodType (R : countRingType) := [countZmodType of polynomial R]. |