diff options
| author | Cyril Cohen | 2019-03-29 13:07:26 +0100 |
|---|---|---|
| committer | GitHub | 2019-03-29 13:07:26 +0100 |
| commit | 850862dc6475bd48524a294651400df4b5b7ecf3 (patch) | |
| tree | 9a00564e1a51d5bc15ddb7ed7a73c14932f387e9 /mathcomp/algebra/matrix.v | |
| parent | 85a3a1ac7f6548a9489fe860d40e5ab110417569 (diff) | |
| parent | c07f1f8d89dd1f975e06e8c45df2c7a4e6ca7fc3 (diff) | |
Merge pull request #292 from erikmd/under-support
Add extra eta lemmas for the under tactic
Diffstat (limited to 'mathcomp/algebra/matrix.v')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 5 |
1 files changed, 5 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. |