diff options
Diffstat (limited to 'mathcomp/algebra/mxalgebra.v')
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 1b6200e..463f07b 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -658,7 +658,7 @@ Qed. Lemma submx_full m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : row_full B -> (A <= B)%MS. Proof. -by rewrite submxE /cokermx =>/eqnP->; rewrite /copid_mx pid_mx_1 subrr !mulmx0. +by rewrite submxE /cokermx => /eqnP->; rewrite /copid_mx pid_mx_1 subrr !mulmx0. Qed. Lemma row_fullP m n (A : 'M_(m, n)) : @@ -700,7 +700,7 @@ Lemma row_full_unit n (A : 'M_n) : row_full A = (A \in unitmx). Proof. exact: row_free_unit. Qed. Lemma mxrank_unit n (A : 'M_n) : A \in unitmx -> \rank A = n. -Proof. by rewrite -row_full_unit =>/eqnP. Qed. +Proof. by rewrite -row_full_unit => /eqnP. Qed. Lemma mxrank1 n : \rank (1%:M : 'M_n) = n. Proof. by apply: mxrank_unit; apply: unitmx1. Qed. @@ -1114,7 +1114,7 @@ Lemma sub_sumsmxP P m n (A : 'M_(m, n)) (B_ : I -> 'M_n) : (A <= \sum_(i | P i) B_ i)%MS. Proof. apply: (iffP idP) => [| [u_ ->]]; last first. - by apply: summx_sub_sums => i _; apply: submxMl. + by apply: summx_sub_sums => i _; apply: submxMl. elim: {P}_.+1 {-2}P A (ltnSn #|P|) => // b IHb P A. case: (pickP P) => [i Pi | P0 _]; last first. rewrite big_pred0 //; move/submx0null->. @@ -1202,7 +1202,7 @@ Lemma mxrank_Frobenius m n p q (A : 'M_(m, n)) B (C : 'M_(p, q)) : Proof. rewrite -{2}(mulmx_base (A *m B)) -mulmxA (eqmxMfull _ (col_base_full _)). set C2 := row_base _ *m C. -rewrite -{1}(subnK (rank_leq_row C2)) -(mxrank_ker C2) addnAC leq_add2r. +rewrite -{1}(subnK (rank_leq_row C2)) -(mxrank_ker C2) addnAC leq_add2r. rewrite addnC -{1}(mulmx_base B) -mulmxA eqmxMfull //. set C1 := _ *m C; rewrite -{2}(subnKC (rank_leq_row C1)) leq_add2l -mxrank_ker. rewrite -(mxrankMfree _ (row_base_free (A *m B))). @@ -1466,7 +1466,7 @@ apply/eqP; set K := kermx B; set C := (A :&: K)%MS. rewrite -(eqmxMr B (eq_row_base A)); set K' := _ *m B. rewrite -{2}(subnKC (rank_leq_row K')) -mxrank_ker eqn_add2l. rewrite -(mxrankMfree _ (row_base_free A)) mxrank_leqif_sup. - rewrite sub_capmx -(eq_row_base A) submxMl. + rewrite sub_capmx -(eq_row_base A) submxMl. by apply/sub_kermxP; rewrite -mulmxA mulmx_ker. have /submxP[C' defC]: (C <= row_base A)%MS by rewrite eq_row_base capmxSl. rewrite defC submxMr //; apply/sub_kermxP. @@ -1573,7 +1573,7 @@ Proof. move=> dxUV sWU; apply/eqP; rewrite -subr_eq0 -submx0 -dxUV. rewrite sub_capmx addmx_sub ?eqmx_opp ?proj_mx_sub //= -eqmx_opp opprB. by rewrite proj_mx_compl_sub // (submx_trans sWU) ?addsmxSl. -Qed. +Qed. Lemma proj_mx_0 m n U V (W : 'M_(m, n)) : (U :&: V = 0)%MS -> (W <= V)%MS -> W *m proj_mx U V = 0. @@ -1845,7 +1845,7 @@ Proof. rewrite /TIsum; apply: (iffP eqnP) => /= [dxS i Pi | dxS]. set Si' := (\sum_(j | _) unwrap (S_ j))%MS. have: mxdirect (unwrap (S_ i) + Si') by apply/eqnP; rewrite /= -!(bigD1 i). - by rewrite mxdirect_addsE => /and3P[-> _ /eqP]. + by rewrite mxdirect_addsE => /and3P[-> _ /eqP]. elim: _.+1 {-2 4}P (subxx P) (ltnSn #|P|) => // m IHm Q; move/subsetP=> sQP. case: (pickP Q) => [i Qi | Q0]; last by rewrite !big_pred0 ?mxrank0. rewrite (cardD1x Qi) !((bigD1 i) Q) //=. |