Put vectors and matrices in two different files. Proved morphism instance for perm_inv and made proofs clearer/nicer.