diff options
| author | Cyril Cohen | 2019-05-29 18:48:38 +0200 |
|---|---|---|
| committer | GitHub | 2019-05-29 18:48:38 +0200 |
| commit | bd4300d26ecbb43f7170e8da7eaaff1a13cc70b1 (patch) | |
| tree | c685f3321960d062eedc51708c3f956d19a40515 /mathcomp/algebra/matrix.v | |
| parent | 6bf8d7707ec6a1d9baf0ce8abaa31f1d681b3b99 (diff) | |
| parent | ccceb6fbd3bd811b728f6e11dad3cf255a577801 (diff) | |
Replace eqVneq to destruct both x == y, but also y == x (#351)
Diffstat (limited to 'mathcomp/algebra/matrix.v')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index d3142d6..9d6e2be 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1392,7 +1392,7 @@ Definition diag_mx n (d : 'rV[R]_n) := \matrix[diag_mx_key]_(i, j) (d 0 i *+ (i == j)). Lemma tr_diag_mx n (d : 'rV_n) : (diag_mx d)^T = diag_mx d. -Proof. by apply/matrixP=> i j; rewrite !mxE eq_sym; case: eqP => // ->. Qed. +Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqVneq => // ->. Qed. Lemma diag_mx_is_linear n : linear (@diag_mx n). Proof. @@ -1744,7 +1744,7 @@ by rewrite eqn_leq andbC leqNgt lshift_subproof. Qed. Lemma tr_pid_mx m n r : (pid_mx r)^T = pid_mx r :> 'M_(n, m). -Proof. by apply/matrixP=> i j; rewrite !mxE eq_sym; case: eqP => // ->. Qed. +Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqVneq => // ->. Qed. Lemma pid_mx_minv m n r : pid_mx (minn m r) = pid_mx r :> 'M_(m, n). Proof. by apply/matrixP=> i j; rewrite !mxE leq_min ltn_ord. Qed. |