proposition: Lemma pinvmxE n (A : 'M[F]_n) : A \in unitmx -> pinvmx A = invmx A.
proof: Proof. move=> A_unit; apply: (@row_free_inj _ _ _ A); rewrite ?row_free_unit//. by rewrite -[pinvmx _]mul1mx mulmxKpV ?sub1mx ?row_full_unit// mulVmx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)