diff options
| author | Cyril Cohen | 2017-12-12 20:10:53 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2017-12-12 20:10:53 +0100 |
| commit | a5878946517d5b07e4273178a939eab66d0ab1f6 (patch) | |
| tree | 8903e0cb3da05bde0479da49b6b9efab392ec3cb /mathcomp | |
| parent | 3e0f4874ce1d421e6a65eb8e745c666cb0313373 (diff) | |
Adding row/col/block_mx_eq0
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 5f47691..dfa8474 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1172,6 +1172,24 @@ Lemma add_block_mx m1 m2 n1 n2 (Aul : 'M_(m1, n1)) Aur Adl (Adr : 'M_(m2, n2)) A + B = block_mx (Aul + Bul) (Aur + Bur) (Adl + Bdl) (Adr + Bdr). Proof. by rewrite /= add_col_mx !add_row_mx. Qed. +Lemma row_mx_eq0 (m n1 n2 : nat) (A1 : 'M_(m, n1)) (A2 : 'M_(m, n2)): + (row_mx A1 A2 == 0) = (A1 == 0) && (A2 == 0). +Proof. +apply/eqP/andP; last by case=> /eqP-> /eqP->; rewrite row_mx0. +by rewrite -row_mx0 => /eq_row_mx [-> ->]. +Qed. + +Lemma col_mx_eq0 (m1 m2 n : nat) (A1 : 'M_(m1, n)) (A2 : 'M_(m2, n)): + (col_mx A1 A2 == 0) = (A1 == 0) && (A2 == 0). +Proof. +by rewrite -) !trmx0 tr_col_mx row_mx_eq0. +Qed. + +Lemma block_mx_eq0 m1 m2 n1 n2 (Aul : 'M_(m1, n1)) Aur Adl (Adr : 'M_(m2, n2)) : + (block_mx Aul Aur Adl Adr == 0) = + [&& Aul == 0, Aur == 0, Adl == 0 & Adr == 0]. +Proof. by rewrite col_mx_eq0 !row_mx_eq0 !andbA. Qed. + Definition nz_row m n (A : 'M_(m, n)) := oapp (fun i => row i A) 0 [pick i | row i A != 0]. |