diff options
| -rw-r--r-- | ChangeLog | 4 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 14 |
2 files changed, 18 insertions, 0 deletions
@@ -26,6 +26,10 @@ * Specialized `bool_irrelevance` so that the statement reflects the name + * Added lemma `eqmxMunitP`: two matrices with the same shape + represent the same subspace iff they differ only by a change of + basis. + 24/04/2018 - compatibility with Coq 8.8 and several small fixes - version 1.7 * Added compatibility with Coq 8.8 and lost compatibility with 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)) : |