proposition: Lemma scalar_mult_matrix_invertible { n } ( i : ⟦ n ⟧%stn ) ( s : F ) ( ne : s != (@rigunel1 F)) : @matrix_inverse F _ (scalar_mult_row_matrix i s).
proof: Proof. exists (scalar_mult_row_matrix i (fldmultinv s ne)). split; refine (scalar_mult_matrix_product _ _ _ @ _); refine (_ @ scalar_mult_matrix_one i); apply maponpaths. - apply fldmultinvrax; assumption. - apply fldmultinvlax; assumption. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.Algebra.Matrix UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.Domains_and_Fields UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors UniMath.Algebra.GaussianElimination.Matrices