proposition: Theorem matrix_inverse_or_non_invertible { n : nat } (A : Matrix F n n) : @matrix_inverse_or_non_invertible_stmt _ _ A.
proof: Proof. unfold matrix_inverse_or_non_invertible_stmt. destruct (natchoice0 n) as [eq0 | gt]. { left; destruct eq0; apply (@nil_matrix_invertible F 0 A). } set (B:= @gauss_clear_all_rows_as_left_matrix _ _ _ A gt). set (BA := B ** A). set (C := upper_triangular_right_inverse_construction BA). assert (ut : is_upper_triangular BA). { unfold BA. pose (is_echelon := @gauss_clear_all_rows_inv3 F _ _ A gt). rewrite <- (gauss_clear_all_rows_as_matrix_eq _ _ gt) in is_echelon. now apply row_echelon_to_upper_triangular. } destruct (vector_all_nonzero_compute _ (λ i : stn n, BA i i)) as [nz | [idx isnotz]]. - left. set (BAC_id := @matrix_right_inverse_construction_inv _ _ ut nz). assert (rinv_eq : (C ** BA) = identity_matrix). { apply (@matrix_right_inverse_implies_left _ _ C (C,, BAC_id)). } exists (C ** B); simpl; use tpair. 2: { simpl; rewrite matrix_mult_assoc; apply rinv_eq. } rewrite <- matrix_mult_assoc. unfold BA in BAC_id. assert (linv_eq : ((B ** A ** C) = (A ** C ** B))). { rewrite matrix_mult_assoc in BAC_id |- *. unfold C in *; clear C; set (C := (upper_triangular_right_inverse_construction BA)). pose (B_rinv := @make_matrix_right_inverse F _ _ n B (A ** C) BAC_id). pose (linv := @matrix_right_inverse_implies_left _ _ C B_rinv). pose (eq := @matrix_left_inverse_equals_right_inverse F n _ n B linv ((A ** C),, BAC_id)). etrans. { change (@matrix_mult F _ _ A _ C) with (pr1 B_rinv). rewrite (pr2 B_rinv); reflexivity. } change (pr1 (@matrix_mult F _ _ A _ C,, BAC_id)) with (@matrix_mult F _ _ A _ C) in *. rewrite <- eq, (pr2 linv). apply idpath. } simpl in * |- ; now rewrite <- BAC_id, <- linv_eq. - right. intros [invM [isl isr]]. pose (isinv := @make_matrix_left_inverse _ _ _ n _ _ isr). assert (isinvprod : (matrix_left_inverse BA)). { apply left_inv_matrix_prod_is_left_inv; try assumption. apply (@matrix_inverse_to_right_and_left_inverse F _ B), gauss_clear_all_rows_matrix_invertible. } pose (contr_eq := @left_invertible_upper_triangular_to_diagonal_all_nonzero _ _ ut isinvprod idx). rewrite isnotz in contr_eq. contradiction. Defined.
imports: UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Nat UniMath.MoreFoundations.Tactics UniMath.Algebra.Matrix UniMath.Algebra.Domains_and_Fields UniMath.Algebra.Matrix UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors UniMath.Algebra.GaussianElimination.Matrices UniMath.Algebra.GaussianElimination.Elimination