proposition: Lemma diagonal_nonzero_iff_transpose_nonzero { n : nat } (A : Matrix R n n) : diagonal_all_nonzero A <-> diagonal_all_nonzero (transpose A).
proof: Proof. split ; intros H; unfold diagonal_all_nonzero, transpose, flip; apply H. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.Matrix UniMath.Algebra.Domains_and_Fields UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors