diff options
| author | Georges Gonthier | 2018-12-11 11:04:45 +0100 |
|---|---|---|
| committer | GitHub | 2018-12-11 11:04:45 +0100 |
| commit | 316cca94aef28c2023cd823c588b140e13d0aded (patch) | |
| tree | 33bfd5ebefbde4b3fef0841d6e039d22104201ab /mathcomp/algebra/mxalgebra.v | |
| parent | 67ccc34eb6f05383e0e7bd90c7df9e4fb51f2a87 (diff) | |
| parent | a2d36f6f0746531d207e760a22d47dd2ebb77ade (diff) | |
Merge pull request #257 from CohenCyril/eqmsP
Adding lemma `eqmxMunitP`
Diffstat (limited to 'mathcomp/algebra/mxalgebra.v')
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index c23d91c..a8a91d3 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -1609,6 +1609,20 @@ rewrite (eqmxMr _ (genmxE U)) injfU genmxE addrC -mulmxDl subrK. by rewrite mul1mx mulVmx ?row_ebase_unit. Qed. +(* Two matrices with the same shape represent the same subspace *) +(* iff they differ only by a change of basis. *) + +Lemma eqmxMunitP m n (U V : 'M_(m, n)) : + reflect (exists2 P, P \in unitmx & U = P *m V) (U == V)%MS. +Proof. +apply: (iffP eqmxP) => [eqUV | [P Punit ->]]; last first. + by apply/eqmxMfull; rewrite row_full_unit. +have [D defU]: exists D, U = D *m V by apply/submxP; rewrite eqUV. +have{eqUV} [Pt Pt_unit defUt]: {Pt | Pt \in unitmx & V^T *m D^T = V^T *m Pt}. + by apply/complete_unitmx; rewrite -trmx_mul -defU !mxrank_tr eqUV. +by exists Pt^T; last apply/trmx_inj; rewrite ?unitmx_tr // defU !trmx_mul trmxK. +Qed. + (* Mapping between two subspaces with the same dimension. *) Lemma eq_rank_unitmx m1 m2 n (U : 'M_(m1, n)) (V : 'M_(m2, n)) : |