proposition: Lemma upper_triangular_iff_transpose_lower_triangular { m n : nat } ( iter : ⟦ n ⟧%stn ) (mat : Matrix R m n) : is_upper_triangular mat <-> is_lower_triangular (transpose mat).
proof: Proof. unfold is_upper_triangular, is_lower_triangular, transpose, flip. split. - intros inv i j i_lt_j. rewrite inv; try assumption; reflexivity. - intros inv i j i_gt_j. rewrite inv; try assumption; reflexivity. 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