diff options
| author | Cyril Cohen | 2020-08-25 00:17:48 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-08 16:24:47 +0200 |
| commit | 4a6bb95c42c3b9097abd80d1201197bccc8bb96d (patch) | |
| tree | 09acbdb12c308521a7184a846c0c1f31fad24251 | |
| parent | be33b7f39bc8885a6d4f38ac5093ce44767fb375 (diff) | |
Adding sub_sums_genmxP (generalizes sub_sumsmxP)
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 1 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 20 |
2 files changed, 15 insertions, 6 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 7823f5e..be208bb 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -104,6 +104,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `mxpoly.v` new lemmas `horner_mx_diag`, `char_poly_trig`, `root_mxminpoly`, and `mxminpoly_diag` +- in `mxalgebra.v`, new lemma `sub_sums_genmxP` (generalizes `sub_sumsmxP`). ### Changed diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index c0c4577..686da21 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -1122,22 +1122,30 @@ Lemma eqmx_sums P n (A B : I -> 'M[F]_n) : (\sum_(i | P i) A i :=: \sum_(i | P i) B i)%MS. Proof. by move=> eqAB; apply/eqmxP; rewrite !sumsmxS // => i; move/eqAB->. Qed. -Lemma sub_sumsmxP P m n (A : 'M_(m, n)) (B_ : I -> 'M_n) : - reflect (exists u_, A = \sum_(i | P i) u_ i *m B_ i) - (A <= \sum_(i | P i) B_ i)%MS. +Lemma sub_sums_genmxP P m n p (A : 'M_(m, p)) (B_ : I -> 'M_(n, p)) : + reflect (exists u_ : I -> 'M_(m, n), A = \sum_(i | P i) u_ i *m B_ i) + (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 _; rewrite genmxE; apply: submxMl. have [b] := ubnP #|P|; elim: b => // b IHb in P A *. case: (pickP P) => [i Pi | P0 _]; last first. rewrite big_pred0 //; move/submx0null->. by exists (fun _ => 0); rewrite big_pred0. -rewrite (cardD1x Pi) (bigD1 i) //= => /IHb{b IHb} /= IHi /sub_addsmxP[u ->]. +rewrite (cardD1x Pi) (bigD1 i) //= => /IHb{b IHb} /= IHi. +rewrite (adds_eqmx (genmxE _) (eqmx_refl _)) => /sub_addsmxP[u ->]. have [u_ ->] := IHi _ (submxMl u.2 _). -exists [eta u_ with i |-> u.1]; rewrite (bigD1 i Pi) /= eqxx; congr (_ + _). +exists [eta u_ with i |-> u.1]; rewrite (bigD1 i Pi)/= eqxx; congr (_ + _). by apply: eq_bigr => j /andP[_ /negPf->]. Qed. +Lemma sub_sumsmxP P m n (A : 'M_(m, n)) (B_ : I -> 'M_n) : + reflect (exists u_, A = \sum_(i | P i) u_ i *m B_ i) + (A <= \sum_(i | P i) B_ i)%MS. +Proof. +by rewrite -(eqmx_sums (fun _ _ => genmxE _)); apply/sub_sums_genmxP. +Qed. + Lemma sumsmxMr_gen P m n A (B : 'M[F]_(m, n)) : ((\sum_(i | P i) A i)%MS *m B :=: \sum_(i | P i) <<A i *m B>>)%MS. Proof. |