proposition: Fact pair_vect_iso : Vector.axiom (dim vT1 + dim vT2) (vT1 * vT2).
proof: Proof. pose p2r (u : vT1 * vT2) := row_mx (v2r u.1) (v2r u.2). pose r2p w := (r2v (lsubmx w) : vT1, r2v (rsubmx w) : vT2). have r2pK : cancel r2p p2r by move=> w; rewrite /p2r !r2vK hsubmxK. have p2rK : cancel p2r r2p by case=> u v; rewrite /r2p row_mxKl row_mxKr !v2rK. have r2p_lin: linear r2p by move=> a u v; congr (_ , _); rewrite /= !linearP. pose r2plM := GRing.isLinear.Build _ _ _ _ r2p r2p_lin. pose r2pL : GRing.Linear.type _ _ := HB.pack r2p r2plM. by exists p2r; [apply: (@can2_linear _ _ _ r2pL) | exists r2p]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)