diff options
| author | Cyril Cohen | 2020-08-25 04:40:09 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-03 03:12:00 +0200 |
| commit | 0bc1691f356145b895012c6f842bfe2783a3e1a2 (patch) | |
| tree | 9782802838e40a328a1a1e9baba247707a39b2e8 /mathcomp/algebra/mxalgebra.v | |
| parent | 56f5dd148ca2728ef69db7ec2f12bc462a73711e (diff) | |
Extracting a nonzero coefficient from a nonzero matrix
+ shortening some proofs
Diffstat (limited to 'mathcomp/algebra/mxalgebra.v')
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 9a0034d..d94bc8e 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -2155,9 +2155,7 @@ rewrite -sum1_card (partition_big lsubmx nzC) => [|A]; last first. rewrite -[A]hsubmxK v0 -[n.+1]/(1 + n)%N -col_mx0. rewrite -[rsubmx _]vsubmxK -det_tr tr_row_mx !tr_col_mx !trmx0. by rewrite det_lblock [0]mx11_scalar det_scalar1 mxE mul0r. -rewrite -sum_nat_const; apply: eq_bigr; rewrite /= -[n.+1]/(1 + n)%N => v nzv. -case: (pickP (fun i => v i 0 != 0)) => [k nza | v0]; last first. - by case/eqP: nzv; apply/colP=> i; move/eqP: (v0 i); rewrite mxE. +rewrite -sum_nat_const; apply: eq_bigr => /= v /cV0Pn[k nza]. have xrkK: involutive (@xrow F _ _ 0 k). by move=> m A /=; rewrite /xrow -row_permM tperm2 row_perm1. rewrite (reindex_inj (inv_inj (xrkK (1 + n)%N))) /= -[n.+1]/(1 + n)%N. |