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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.GaussianElimination.Auxiliary. Require Import UniMath.Algebra.GaussianElimination.Vectors. Require Import UniMath.Algebra.GaussianElimination.Matrices.