Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.Decidable.Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.Decidable.
Require Import Types.Sigma.
Require Import Spaces.List.Core Spaces.List.Theory Spaces.List.Paths.
Require Import Algebra.Rings.Ring Algebra.Rings.Module Algebra.Rings.CRing
  Algebra.Rings.KroneckerDelta Algebra.Rings.Vector.
Require Import abstract_algebra.
Require Import WildCat.Core WildCat.Paths.
Require Import Modalities.ReflectiveSubuniverse.

Set Universe Minimization ToSet.

(** * Matrices *)

(** ** Definition *)

Definition Matrix@{i} (R : Type@{i}) (m n : nat) : Type@{i}
  := Vector (Vector R n) m.

Instance istrunc_matrix (R : Type) k `{IsTrunc k.+2 R} m n
  : IsTrunc k.+2 (Matrix R m n)
  := _.

(** Building a matrix from a function that takes row and column indices. *)
Definition Build_Matrix (R : Type) (m n : nat)
  (M_fun : forall (i : nat) (j : nat), (i < m)%nat -> (j < n)%nat -> R)
  : Matrix R m n.
R: Type
m, n: nat
M_fun: forall i j : nat, (i < m)%nat -> (j < n)%nat -> R
Matrix R m n
Proof.
R: Type
m, n: nat
M_fun: forall i j : nat, (i < m)%nat -> (j < n)%nat -> R
Matrix R m n
  snapply Build_Vector.
R: Type
m, n: nat
M_fun: forall i j : nat, (i < m)%nat -> (j < n)%nat -> R
forall i : nat, (i < m)%nat -> Vector R n
  intros i Hi.
R: Type
m, n: nat
M_fun: forall i0 j : nat, (i0 < m)%nat -> (j < n)%nat -> R
i: nat
Hi: (i < m)%nat
Vector R n
  snapply Build_Vector.
R: Type
m, n: nat
M_fun: forall i0 j : nat, (i0 < m)%nat -> (j < n)%nat -> R
i: nat
Hi: (i < m)%nat
forall i0 : nat, (i0 < n)%nat -> R
  intros j Hj.
R: Type
m, n: nat
M_fun: forall i0 j0 : nat, (i0 < m)%nat -> (j0 < n)%nat -> R
i: nat
Hi: (i < m)%nat
j: nat
Hj: (j < n)%nat
R
  exact (M_fun i j Hi Hj).
Defined.

(** The length conditions here are decidable so can be inferred in proofs. *)
Definition Build_Matrix' (R : Type) (m n : nat)
  (l : list (list R))
  (wf_row : length l = m)
  (wf_col : for_all (fun row => length row = n) l)
  : Matrix R m n.
R: Type
m, n: nat
l: list (list R)
wf_row: length l = m
wf_col: for_all (fun row : list R => length row = n) l
Matrix R m n
Proof.
R: Type
m, n: nat
l: list (list R)
wf_row: length l = m
wf_col: for_all (fun row : list R => length row = n) l
Matrix R m n
  snrefine (_; _).
R: Type
m, n: nat
l: list (list R)
wf_row: length l = m
wf_col: for_all (fun row : list R => length row = n) l
list (Vector R n)
R: Type
m, n: nat
l: list (list R)
wf_row: length l = m
wf_col: for_all (fun row : list R => length row = n) l
(fun l0 : list (Vector R n) => length l0 = m) ?proj1
  -
R: Type
m, n: nat
l: list (list R)
wf_row: length l = m
wf_col: for_all (fun row : list R => length row = n) l
list (Vector R n) snapply list_sigma.
R: Type
m, n: nat
l: list (list R)
wf_row: length l = m
wf_col: for_all (fun row : list R => length row = n) l
list (list R)
R: Type
m, n: nat
l: list (list R)
wf_row: length l = m
wf_col: for_all (fun row : list R => length row = n) l
for_all (fun x : list R => length x = n) ?l
    +
R: Type
m, n: nat
l: list (list R)
wf_row: length l = m
wf_col: for_all (fun row : list R => length row = n) l
list (list R) exact l.
    +
R: Type
m, n: nat
l: list (list R)
wf_row: length l = m
wf_col: for_all (fun row : list R => length row = n) l
for_all (fun x : list R => length x = n) l exact wf_col.
  -
R: Type
m, n: nat
l: list (list R)
wf_row: length l = m
wf_col: for_all (fun row : list R => length row = n) l
(fun l0 : list (Vector R n) => length l0 = m)
  (list_sigma (fun x : list R => length x = n) l wf_col) by lhs napply length_list_sigma.
Defined.

Definition entries@{i|} {R : Type@{i}} {m n} (M : Matrix R m n)
  : list (list R)
  := list_map@{i i} pr1 (pr1 M).

(** The entry at row [i] and column [j] of a matrix [M]. *)
Definition entry {R : Type} {m n} (M : Matrix R m n) (i j : nat)
  {H1 : (i < m)%nat} {H2 : (j < n)%nat}
  : R
  := Vector.entry (Vector.entry M i) j.

(** Mapping a function on all the entries of a matrix. *)
Definition matrix_map {R S : Type} {m n} (f : R -> S)
  : Matrix R m n -> Matrix S m n
  := fun M => Build_Matrix S m n (fun i j _ _ => f (entry M i j)).

Definition matrix_map2 {R S T : Type} {m n} (f : R -> S -> T)
  : Matrix R m n -> Matrix S m n -> Matrix T m n
  := fun M N => Build_Matrix T m n
    (fun i j _ _ => f (entry M i j) (entry N i j)).

(** The [(i, j)]-entry of [Build_Matrix R m n M_fun] is [M_fun i j]. *)
Definition entry_Build_Matrix {R : Type} {m n}
  (M_fun : forall i j, (i < m)%nat -> (j < n)%nat -> R)
  (i j : nat) (H1 : (i < m)%nat) (H2 : (j < n)%nat)
  : entry (Build_Matrix R m n M_fun) i j = M_fun i j _ _.
R: Type
m, n: nat
M_fun: forall i0 j0 : nat, (i0 < m)%nat -> (j0 < n)%nat -> R
i, j: nat
H1: (i < m)%nat
H2: (j < n)%nat
entry (Build_Matrix R m n M_fun) i j = M_fun i j H1 H2
Proof.
R: Type
m, n: nat
M_fun: forall i0 j0 : nat, (i0 < m)%nat -> (j0 < n)%nat -> R
i, j: nat
H1: (i < m)%nat
H2: (j < n)%nat
entry (Build_Matrix R m n M_fun) i j = M_fun i j H1 H2
  unfold entry.
R: Type
m, n: nat
M_fun: forall i0 j0 : nat, (i0 < m)%nat -> (j0 < n)%nat -> R
i, j: nat
H1: (i < m)%nat
H2: (j < n)%nat
Vector.entry (Vector.entry (Build_Matrix R m n M_fun) i) j = M_fun i j H1 H2
  by rewrite 2 entry_Build_Vector.
Defined.

(** Two matrices are equal if all their entries are equal. *)
Definition path_matrix {R : Type} {m n} (M N : Matrix R m n)
  (H : forall i j (Hi : (i < m)%nat) (Hj : (j < n)%nat), entry M i j = entry N i j)
  : M = N.
R: Type
m, n: nat
M, N: Matrix R m n
H: forall (i j : nat) (Hi : (i < m)%nat) (Hj : (j < n)%nat),
entry M i j = entry N i j
M = N
Proof.
R: Type
m, n: nat
M, N: Matrix R m n
H: forall (i j : nat) (Hi : (i < m)%nat) (Hj : (j < n)%nat),
entry M i j = entry N i j
M = N
  snapply path_vector.
R: Type
m, n: nat
M, N: Matrix R m n
H: forall (i j : nat) (Hi : (i < m)%nat) (Hj : (j < n)%nat),
entry M i j = entry N i j
forall (i : nat) (H0 : (i < m)%nat), Vector.entry M i = Vector.entry N i
  intros i Hi.
R: Type
m, n: nat
M, N: Matrix R m n
H: forall (i0 j : nat) (Hi0 : (i0 < m)%nat) (Hj : (j < n)%nat),
entry M i0 j = entry N i0 j
i: nat
Hi: (i < m)%nat
Vector.entry M i = Vector.entry N i
  snapply path_vector.
R: Type
m, n: nat
M, N: Matrix R m n
H: forall (i0 j : nat) (Hi0 : (i0 < m)%nat) (Hj : (j < n)%nat),
entry M i0 j = entry N i0 j
i: nat
Hi: (i < m)%nat
forall (i0 : nat) (H0 : (i0 < n)%nat),
Vector.entry (Vector.entry M i) i0 = Vector.entry (Vector.entry N i) i0
  intros j Hj.
R: Type
m, n: nat
M, N: Matrix R m n
H: forall (i0 j0 : nat) (Hi0 : (i0 < m)%nat) (Hj0 : (j0 < n)%nat),
entry M i0 j0 = entry N i0 j0
i: nat
Hi: (i < m)%nat
j: nat
Hj: (j < n)%nat
Vector.entry (Vector.entry M i) j = Vector.entry (Vector.entry N i) j
  exact (H i j Hi Hj).
Defined.

(** ** Addition and module structure *)

(** Here we define the abelian group of (n x m)-matrices over a ring. This follows from the abelian group structure of the underlying vectors. We are also able to derive a left module structure when the entries come from a left module. *)

Definition abgroup_matrix (A : AbGroup) (m n : nat) : AbGroup
  := abgroup_vector (abgroup_vector A n) m.

Definition matrix_plus {A : AbGroup} {m n}
  : Matrix A m n -> Matrix A m n -> Matrix A m n
  := @sg_op (abgroup_matrix A m n) _.

Definition matrix_zero (A : AbGroup) m n : Matrix A m n
  := @mon_unit (abgroup_matrix A m n) _.

Definition matrix_negate {A : AbGroup} {m n}
  : Matrix A m n -> Matrix A m n
  := @negate (abgroup_matrix A m n) _.

Instance isleftmodule_isleftmodule_matrix (A : AbGroup) (m n : nat)
  {R : Ring} `{IsLeftModule R A}
  : IsLeftModule R (abgroup_matrix A m n).
A: AbGroup
m, n: nat
R: Ring
H: IsLeftModule R A
IsLeftModule R (abgroup_matrix A m n)
Proof.
A: AbGroup
m, n: nat
R: Ring
H: IsLeftModule R A
IsLeftModule R (abgroup_matrix A m n)
  snapply isleftmodule_isleftmodule_vector.
A: AbGroup
m, n: nat
R: Ring
H: IsLeftModule R A
IsLeftModule R (abgroup_vector A n)
  snapply isleftmodule_isleftmodule_vector.
A: AbGroup
m, n: nat
R: Ring
H: IsLeftModule R A
IsLeftModule R A
  exact _.
Defined.

(** As a special case, we get the left module of matrices over a ring. *)
Instance isleftmodule_abgroup_matrix (R : Ring) (m n : nat)
  : IsLeftModule R (abgroup_matrix R m n)
  := _.

Definition matrix_lact {R : Ring} {m n : nat} (r : R) (M : Matrix R m n)
  : Matrix R m n
  := lact r M.  

(** ** Multiplication *)

(** Matrix multiplication is defined such that the entry at row [i] and column [j] of the resulting matrix is the sum of the products of the corresponding entries from the [i]th row of the first matrix and the [j]th column of the second matrix. Matrices correspond to module homomorphisms between free modules of finite rank (think vector spaces), and matrix multiplication represents the composition of these homomorphisms. **)
Definition matrix_mult {R : Ring@{i}} {m n k : nat} (M : Matrix R m n) (N : Matrix R n k)
  : Matrix R m k.
R: Ring
m, n, k: nat
M: Matrix R m n
N: Matrix R n k
Matrix R m k
Proof.
R: Ring
m, n, k: nat
M: Matrix R m n
N: Matrix R n k
Matrix R m k
  snapply Build_Matrix.
R: Ring
m, n, k: nat
M: Matrix R m n
N: Matrix R n k
forall i j : nat, (i < m)%nat -> (j < k)%nat -> R
  intros i j Hi Hj.
R: Ring
m, n, k: nat
M: Matrix R m n
N: Matrix R n k
i, j: nat
Hi: (i < m)%nat
Hj: (j < k)%nat
R
  exact (ab_sum n (fun k Hk => entry M i k * entry N k j)).
Defined.

(** The identity matrix is the matrix with ones on the diagonal and zeros elsewhere. It acts as the multiplicative identity for matrix multiplication. We define it here using the [kronecker_delta] function which will make proving properties about it conceptually easier later. *)
Definition identity_matrix (R : Ring@{i}) (n : nat) : Matrix R n n
  := Build_Matrix R n n (fun i j _ _ => kronecker_delta i j).

(** This is the most general statement of associativity for matrix multiplication. *)
Definition associative_matrix_mult (R : Ring) (m n p q : nat)
  : HeteroAssociative
      (@matrix_mult R m n q) (@matrix_mult R n p q)
      (@matrix_mult R m p q) (@matrix_mult R m n p).
R: Ring
m, n, p, q: nat
HeteroAssociative matrix_mult matrix_mult matrix_mult matrix_mult
Proof.
R: Ring
m, n, p, q: nat
HeteroAssociative matrix_mult matrix_mult matrix_mult matrix_mult
  intros M N P; napply path_matrix; intros i j Hi Hj.
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
entry (matrix_mult M (matrix_mult N P)) i j =
entry (matrix_mult (matrix_mult M N) P) i j
  rewrite 2 entry_Build_Matrix.
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   entry M i k * entry (matrix_mult N P) k j) =
ab_sum p
  (fun (k : nat) (Hk : (k < p)%nat) =>
   entry (matrix_mult M N) i k * entry P k j)
  lhs napply path_ab_sum.
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
forall (k : nat) (Hk : (k < n)%nat),
entry M i k * entry (matrix_mult N P) k j = ?Goal k Hk
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
ab_sum n ?Goal =
ab_sum p
  (fun (k : nat) (Hk : (k < p)%nat) =>
   entry (matrix_mult M N) i k * entry P k j)
  {
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
forall (k : nat) (Hk : (k < n)%nat),
entry M i k * entry (matrix_mult N P) k j = ?Goal k Hk intros k Hk.
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
k: nat
Hk: (k < n)%nat
entry M i k * entry (matrix_mult N P) k j = ?Goal k Hk
    rewrite entry_Build_Matrix.
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
k: nat
Hk: (k < n)%nat
entry M i k *
ab_sum p (fun (k0 : nat) (Hk0 : (k0 < p)%nat) => entry N k k0 * entry P k0 j) =
?Goal k Hk
    apply rng_sum_dist_l. }
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   ab_sum p
     (fun (k0 : nat) (Hk0 : (k0 < p)%nat) =>
      entry M i k *
      (fun (k1 : nat) (Hk1 : (k1 < p)%nat) => entry N k k1 * entry P k1 j) k0
        Hk0)) =
ab_sum p
  (fun (k : nat) (Hk : (k < p)%nat) =>
   entry (matrix_mult M N) i k * entry P k j)
  lhs napply ab_sum_sum.
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
ab_sum p
  (fun (j0 : nat) (Hj0 : (j0 < p)%nat) =>
   ab_sum n
     (fun (i0 : nat) (Hi0 : (i0 < n)%nat) =>
      entry M i i0 * (entry N i0 j0 * entry P j0 j))) =
ab_sum p
  (fun (k : nat) (Hk : (k < p)%nat) =>
   entry (matrix_mult M N) i k * entry P k j)
  rhs napply path_ab_sum.
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
ab_sum p
  (fun (j0 : nat) (Hj0 : (j0 < p)%nat) =>
   ab_sum n
     (fun (i0 : nat) (Hi0 : (i0 < n)%nat) =>
      entry M i i0 * (entry N i0 j0 * entry P j0 j))) =
ab_sum p ?Goal
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
forall (k : nat) (Hk : (k < p)%nat),
entry (matrix_mult M N) i k * entry P k j = ?Goal k Hk
  2: intros k Hk; by rewrite entry_Build_Matrix.
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
ab_sum p
  (fun (j0 : nat) (Hj0 : (j0 < p)%nat) =>
   ab_sum n
     (fun (i0 : nat) (Hi0 : (i0 < n)%nat) =>
      entry M i i0 * (entry N i0 j0 * entry P j0 j))) =
ab_sum p
  (fun (k : nat) (Hk : (k < p)%nat) =>
   ab_sum n
     (fun (k0 : nat) (Hk0 : (k0 < n)%nat) => entry M i k0 * entry N k0 k) *
   entry P k j)
  napply path_ab_sum.
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
forall (k : nat) (Hk : (k < p)%nat),
ab_sum n
  (fun (i0 : nat) (Hi0 : (i0 < n)%nat) =>
   entry M i i0 * (entry N i0 k * entry P k j)) =
ab_sum n (fun (k0 : nat) (Hk0 : (k0 < n)%nat) => entry M i k0 * entry N k0 k) *
entry P k j
  intros k Hk.
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
k: nat
Hk: (k < p)%nat
ab_sum n
  (fun (i0 : nat) (Hi0 : (i0 < n)%nat) =>
   entry M i i0 * (entry N i0 k * entry P k j)) =
ab_sum n (fun (k0 : nat) (Hk0 : (k0 < n)%nat) => entry M i k0 * entry N k0 k) *
entry P k j
  rhs napply rng_sum_dist_r.
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
k: nat
Hk: (k < p)%nat
ab_sum n
  (fun (i0 : nat) (Hi0 : (i0 < n)%nat) =>
   entry M i i0 * (entry N i0 k * entry P k j)) =
ab_sum n
  (fun (k0 : nat) (Hk0 : (k0 < n)%nat) =>
   entry M i k0 * entry N k0 k * entry P k j)
  napply path_ab_sum.
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
k: nat
Hk: (k < p)%nat
forall (k0 : nat) (Hk0 : (k0 < n)%nat),
entry M i k0 * (entry N k0 k * entry P k j) =
entry M i k0 * entry N k0 k * entry P k j
  intros l Hl.
R: Ring
m, n, p, q: nat
M: Matrix R m n
N: Matrix R n p
P: Matrix R p q
i, j: nat
Hi: (i < m)%nat
Hj: (j < q)%nat
k: nat
Hk: (k < p)%nat
l: nat
Hl: (l < n)%nat
entry M i l * (entry N l k * entry P k j) =
entry M i l * entry N l k * entry P k j
  apply associativity.
Defined.

(** Matrix multiplication distributes over addition of matrices on the left. *)
Definition left_distribute_matrix_mult (R : Ring) (m n p : nat)
  : LeftHeteroDistribute (@matrix_mult R m n p) matrix_plus matrix_plus.
R: Ring
m, n, p: nat
LeftHeteroDistribute matrix_mult matrix_plus matrix_plus
Proof.
R: Ring
m, n, p: nat
LeftHeteroDistribute matrix_mult matrix_plus matrix_plus
  intros M N P; apply path_matrix; intros i j Hi Hj.
R: Ring
m, n, p: nat
M: Matrix R m n
N, P: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
entry (matrix_mult M (matrix_plus N P)) i j =
entry (matrix_plus (matrix_mult M N) (matrix_mult M P)) i j
  rewrite !entry_Build_Matrix, !entry_Build_Vector.
R: Ring
m, n, p: nat
M: Matrix R m n
N, P: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   entry M i k * entry (matrix_plus N P) k j) =
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => entry M i k * entry N k j) +
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => entry M i k * entry P k j)
  change (?x = ?y + ?z) with (x = sg_op y z).
R: Ring
m, n, p: nat
M: Matrix R m n
N, P: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   entry M i k * entry (matrix_plus N P) k j) =
sg_op
  (ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => entry M i k * entry N k j))
  (ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => entry M i k * entry P k j))
  rewrite <- ab_sum_plus.
R: Ring
m, n, p: nat
M: Matrix R m n
N, P: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   entry M i k * entry (matrix_plus N P) k j) =
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   sg_op (entry M i k * entry N k j) (entry M i k * entry P k j))
  napply path_ab_sum.
R: Ring
m, n, p: nat
M: Matrix R m n
N, P: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
forall (k : nat) (Hk : (k < n)%nat),
entry M i k * entry (matrix_plus N P) k j =
sg_op (entry M i k * entry N k j) (entry M i k * entry P k j)
  intros k Hk.
R: Ring
m, n, p: nat
M: Matrix R m n
N, P: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
k: nat
Hk: (k < n)%nat
entry M i k * entry (matrix_plus N P) k j =
sg_op (entry M i k * entry N k j) (entry M i k * entry P k j)
  rewrite entry_Build_Matrix.
R: Ring
m, n, p: nat
M: Matrix R m n
N, P: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
k: nat
Hk: (k < n)%nat
entry M i k *
(Vector.entry (Vector.entry N k) j + Vector.entry (Vector.entry P k) j) =
sg_op (entry M i k * entry N k j) (entry M i k * entry P k j)
  apply rng_dist_l.
Defined.

(** Matrix multiplication distributes over addition of matrices on the right. *)
Definition right_distribute_matrix_mult (R : Ring) (m n p : nat)
  : RightHeteroDistribute (@matrix_mult R m n p) matrix_plus matrix_plus.
R: Ring
m, n, p: nat
RightHeteroDistribute matrix_mult matrix_plus matrix_plus
Proof.
R: Ring
m, n, p: nat
RightHeteroDistribute matrix_mult matrix_plus matrix_plus
  intros M N P; apply path_matrix; intros i j Hi Hj.
R: Ring
m, n, p: nat
M, N: Matrix R m n
P: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
entry (matrix_mult (matrix_plus M N) P) i j =
entry (matrix_plus (matrix_mult M P) (matrix_mult N P)) i j
  rewrite !entry_Build_Matrix, !entry_Build_Vector.
R: Ring
m, n, p: nat
M, N: Matrix R m n
P: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   entry (matrix_plus M N) i k * entry P k j) =
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => entry M i k * entry P k j) +
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => entry N i k * entry P k j)
  change (?x = ?y + ?z) with (x = sg_op y z).
R: Ring
m, n, p: nat
M, N: Matrix R m n
P: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   entry (matrix_plus M N) i k * entry P k j) =
sg_op
  (ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => entry M i k * entry P k j))
  (ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => entry N i k * entry P k j))
  rewrite <- ab_sum_plus.
R: Ring
m, n, p: nat
M, N: Matrix R m n
P: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   entry (matrix_plus M N) i k * entry P k j) =
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   sg_op (entry M i k * entry P k j) (entry N i k * entry P k j))
  napply path_ab_sum.
R: Ring
m, n, p: nat
M, N: Matrix R m n
P: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
forall (k : nat) (Hk : (k < n)%nat),
entry (matrix_plus M N) i k * entry P k j =
sg_op (entry M i k * entry P k j) (entry N i k * entry P k j)
  intros k Hk.
R: Ring
m, n, p: nat
M, N: Matrix R m n
P: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
k: nat
Hk: (k < n)%nat
entry (matrix_plus M N) i k * entry P k j =
sg_op (entry M i k * entry P k j) (entry N i k * entry P k j)
  rewrite entry_Build_Matrix.
R: Ring
m, n, p: nat
M, N: Matrix R m n
P: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
k: nat
Hk: (k < n)%nat
(Vector.entry (Vector.entry M i) k + Vector.entry (Vector.entry N i) k) *
entry P k j = sg_op (entry M i k * entry P k j) (entry N i k * entry P k j)
  apply rng_dist_r.
Defined.

(** The identity matrix acts as a left identity for matrix multiplication. *)
Definition left_identity_matrix_mult (R : Ring) (m n: nat)
  : LeftIdentity (@matrix_mult R m m n) (identity_matrix R m).
R: Ring
m, n: nat
LeftIdentity matrix_mult (identity_matrix R m)
Proof.
R: Ring
m, n: nat
LeftIdentity matrix_mult (identity_matrix R m)
  intros M; apply path_matrix; intros i j Hi Hj.
R: Ring
m, n: nat
M: Matrix R m n
i, j: nat
Hi: (i < m)%nat
Hj: (j < n)%nat
entry (matrix_mult (identity_matrix R m) M) i j = entry M i j
  rewrite entry_Build_Matrix.
R: Ring
m, n: nat
M: Matrix R m n
i, j: nat
Hi: (i < m)%nat
Hj: (j < n)%nat
ab_sum m
  (fun (k : nat) (Hk : (k < m)%nat) =>
   entry (identity_matrix R m) i k * entry M k j) =
entry M i j
  lhs napply path_ab_sum.
R: Ring
m, n: nat
M: Matrix R m n
i, j: nat
Hi: (i < m)%nat
Hj: (j < n)%nat
forall (k : nat) (Hk : (k < m)%nat),
entry (identity_matrix R m) i k * entry M k j = ?Goal k Hk
R: Ring
m, n: nat
M: Matrix R m n
i, j: nat
Hi: (i < m)%nat
Hj: (j < n)%nat
ab_sum m ?Goal = entry M i j
  1: intros k Hk; by rewrite entry_Build_Matrix.
R: Ring
m, n: nat
M: Matrix R m n
i, j: nat
Hi: (i < m)%nat
Hj: (j < n)%nat
ab_sum m
  (fun (k : nat) (Hk : (k < m)%nat) => kronecker_delta i k * entry M k j) =
entry M i j
  napply rng_sum_kronecker_delta_l.
Defined.

(** The identity matrix acts as a right identity for matrix multiplication. *)
Definition right_identity_matrix_mult (R : Ring) (m n : nat)
  : RightIdentity (@matrix_mult R m n n) (identity_matrix R n).
R: Ring
m, n: nat
RightIdentity matrix_mult (identity_matrix R n)
Proof.
R: Ring
m, n: nat
RightIdentity matrix_mult (identity_matrix R n)
  intros M; apply path_matrix; intros i j Hi Hj.
R: Ring
m, n: nat
M: Matrix R m n
i, j: nat
Hi: (i < m)%nat
Hj: (j < n)%nat
entry (matrix_mult M (identity_matrix R n)) i j = entry M i j
  rewrite entry_Build_Matrix.
R: Ring
m, n: nat
M: Matrix R m n
i, j: nat
Hi: (i < m)%nat
Hj: (j < n)%nat
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   entry M i k * entry (identity_matrix R n) k j) =
entry M i j
  lhs napply path_ab_sum.
R: Ring
m, n: nat
M: Matrix R m n
i, j: nat
Hi: (i < m)%nat
Hj: (j < n)%nat
forall (k : nat) (Hk : (k < n)%nat),
entry M i k * entry (identity_matrix R n) k j = ?Goal k Hk
R: Ring
m, n: nat
M: Matrix R m n
i, j: nat
Hi: (i < m)%nat
Hj: (j < n)%nat
ab_sum n ?Goal = entry M i j
  1: intros k Hk; by rewrite entry_Build_Matrix.
R: Ring
m, n: nat
M: Matrix R m n
i, j: nat
Hi: (i < m)%nat
Hj: (j < n)%nat
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) => entry M i k * kronecker_delta k j) =
entry M i j
  napply rng_sum_kronecker_delta_r'.
Defined.

(** TODO: define this as an R-algebra. What is an R-algebra over a non-commutative right however? (Here we have a bimodule which might be important) *)
(** Matrices over a ring form a (generally) non-commutative ring. *)
Definition matrix_ring (R : Ring@{i}) (n : nat) : Ring.
R: Ring
n: nat
Ring
Proof.
R: Ring
n: nat
Ring
  snapply Build_Ring.
R: Ring
n: nat
AbGroup
R: Ring
n: nat
Mult ?R
R: Ring
n: nat
One ?R
R: Ring
n: nat
Associative mult
R: Ring
n: nat
LeftDistribute mult plus
R: Ring
n: nat
RightDistribute mult plus
R: Ring
n: nat
LeftIdentity mult 1
R: Ring
n: nat
RightIdentity mult 1
  -
R: Ring
n: nat
AbGroup exact (abgroup_matrix R n n).
  -
R: Ring
n: nat
Mult (abgroup_matrix R n n) exact matrix_mult.
  -
R: Ring
n: nat
One (abgroup_matrix R n n) exact (identity_matrix R n).
  -
R: Ring
n: nat
Associative mult exact (associative_matrix_mult R n n n n).
  -
R: Ring
n: nat
LeftDistribute mult plus exact (left_distribute_matrix_mult R n n n).
  -
R: Ring
n: nat
RightDistribute mult plus exact (right_distribute_matrix_mult R n n n).
  -
R: Ring
n: nat
LeftIdentity mult 1 exact (left_identity_matrix_mult R n n).
  -
R: Ring
n: nat
RightIdentity mult 1 exact (right_identity_matrix_mult R n n).
Defined.

(** Matrix multiplication on the right preserves scalar multiplication in the sense that [matrix_lact r (matrix_mult M N) = matrix_mult (matrix_lact r M) N] for [r] a ring element and [M] and [N] matrices of compatible sizes. *)
Definition matrix_mult_lact_l {R : Ring} {m n p : nat}
  : HeteroAssociative (@matrix_lact R m p) (@matrix_mult R m n p)
      (@matrix_mult R m n p) (@matrix_lact R m n).
R: Ring
m, n, p: nat
HeteroAssociative matrix_lact matrix_mult matrix_mult matrix_lact
Proof.
R: Ring
m, n, p: nat
HeteroAssociative matrix_lact matrix_mult matrix_mult matrix_lact
  intros r M N.
R: Ring
m, n, p: nat
r: R
M: Matrix R m n
N: Matrix R n p
matrix_lact r (matrix_mult M N) = matrix_mult (matrix_lact r M) N
  snapply path_matrix.
R: Ring
m, n, p: nat
r: R
M: Matrix R m n
N: Matrix R n p
forall (i j : nat) (Hi : (i < m)%nat) (Hj : (j < p)%nat),
entry (matrix_lact r (matrix_mult M N)) i j =
entry (matrix_mult (matrix_lact r M) N) i j
  intros i j Hi Hj.
R: Ring
m, n, p: nat
r: R
M: Matrix R m n
N: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
entry (matrix_lact r (matrix_mult M N)) i j =
entry (matrix_mult (matrix_lact r M) N) i j
  rewrite !entry_Build_Matrix, !entry_Build_Vector.
R: Ring
m, n, p: nat
r: R
M: Matrix R m n
N: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
lact r
  (ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => entry M i k * entry N k j)) =
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   entry (matrix_lact r M) i k * entry N k j) 
  lhs napply rng_sum_dist_l.
R: Ring
m, n, p: nat
r: R
M: Matrix R m n
N: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) => r * (entry M i k * entry N k j)) =
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   entry (matrix_lact r M) i k * entry N k j)
  snapply path_ab_sum.
R: Ring
m, n, p: nat
r: R
M: Matrix R m n
N: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
forall (k : nat) (Hk : (k < n)%nat),
(fun (k0 : nat) (Hk0 : (k0 < n)%nat) => r * (entry M i k0 * entry N k0 j)) k
  Hk =
(fun (k0 : nat) (Hk0 : (k0 < n)%nat) =>
 entry (matrix_lact r M) i k0 * entry N k0 j) k Hk
  intros k Hk; cbn.
R: Ring
m, n, p: nat
r: R
M: Matrix R m n
N: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
k: nat
Hk: (k < n)%nat
r * (entry M i k * entry N k j) = entry (vector_lact r M) i k * entry N k j
  rewrite !entry_Build_Matrix.
R: Ring
m, n, p: nat
r: R
M: Matrix R m n
N: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
k: nat
Hk: (k < n)%nat
r * (entry M i k * entry N k j) =
lact r (Vector.entry (Vector.entry M i) k) * entry N k j
  snapply rng_mult_assoc.
Defined.

(** The same doesn't hold for the right matrix, since the ring is not commutative. However we could say an analogous statement for the right action. We haven't yet stated a definition of right module yet though. *)

(** In a commutative ring, matrix multiplication over the ring and the opposite ring agree. *)
Definition matrix_mult_rng_op {R : CRing} {m n p}
  (M : Matrix R m n) (N : Matrix R n p)
  : matrix_mult (R:=rng_op R) M N = matrix_mult M N.
R: CRing
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
matrix_mult M N = matrix_mult M N
Proof.
R: CRing
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
matrix_mult M N = matrix_mult M N
  apply path_matrix; intros i j Hi Hj.
R: CRing
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
entry (matrix_mult M N) i j = entry (matrix_mult M N) i j
  rewrite 2 entry_Build_Matrix.
R: CRing
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => entry M i k * entry N k j) =
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => entry M i k * entry N k j)
  apply path_ab_sum; intros k Hk.
R: CRing
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
i, j: nat
Hi: (i < m)%nat
Hj: (j < p)%nat
k: nat
Hk: (k < n)%nat
entry M i k * entry N k j = entry M i k * entry N k j
  apply rng_mult_comm.
Defined.

(** ** Transpose *)

(** The transpose of a matrix is the matrix with the rows and columns swapped. *)
Definition matrix_transpose {R : Type} {m n} : Matrix R m n -> Matrix R n m
  := fun M => Build_Matrix R n m (fun i j H1 H2 => entry M j i).

(** Transposing a matrix is involutive. *)
Definition matrix_transpose_transpose {R : Type} {m n} (M : Matrix R m n)
  : matrix_transpose (matrix_transpose M) = M.
R: Type
m, n: nat
M: Matrix R m n
matrix_transpose (matrix_transpose M) = M
Proof.
R: Type
m, n: nat
M: Matrix R m n
matrix_transpose (matrix_transpose M) = M
  apply path_matrix.
R: Type
m, n: nat
M: Matrix R m n
forall (i j : nat) (Hi : (i < m)%nat) (Hj : (j < n)%nat),
entry (matrix_transpose (matrix_transpose M)) i j = entry M i j
  intros i j Hi Hj.
R: Type
m, n: nat
M: Matrix R m n
i, j: nat
Hi: (i < m)%nat
Hj: (j < n)%nat
entry (matrix_transpose (matrix_transpose M)) i j = entry M i j
  lhs napply entry_Build_Matrix.
R: Type
m, n: nat
M: Matrix R m n
i, j: nat
Hi: (i < m)%nat
Hj: (j < n)%nat
entry (matrix_transpose M) j i = entry M i j
  napply entry_Build_Matrix.
Defined.

(** Transpose distributes over addition. *)
Definition matrix_transpose_plus {R : Ring} {m n} (M N : Matrix R m n)
  : matrix_transpose (matrix_plus M N)
    = matrix_plus (matrix_transpose M) (matrix_transpose N).
R: Ring
m, n: nat
M, N: Matrix R m n
matrix_transpose (matrix_plus M N) =
matrix_plus (matrix_transpose M) (matrix_transpose N)
Proof.
R: Ring
m, n: nat
M, N: Matrix R m n
matrix_transpose (matrix_plus M N) =
matrix_plus (matrix_transpose M) (matrix_transpose N)
  apply path_matrix.
R: Ring
m, n: nat
M, N: Matrix R m n
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < m)%nat),
entry (matrix_transpose (matrix_plus M N)) i j =
entry (matrix_plus (matrix_transpose M) (matrix_transpose N)) i j
  intros i j Hi Hj.
R: Ring
m, n: nat
M, N: Matrix R m n
i, j: nat
Hi: (i < n)%nat
Hj: (j < m)%nat
entry (matrix_transpose (matrix_plus M N)) i j =
entry (matrix_plus (matrix_transpose M) (matrix_transpose N)) i j
  by rewrite !entry_Build_Matrix, !entry_Build_Vector.
Defined.

(** Transpose commutes with scalar multiplication. *)
Definition matrix_transpose_lact {R : Ring} {m n} (r : R) (M : Matrix R m n)
  : matrix_transpose (matrix_lact r M)
    = matrix_lact r (matrix_transpose M).
R: Ring
m, n: nat
r: R
M: Matrix R m n
matrix_transpose (matrix_lact r M) = matrix_lact r (matrix_transpose M)
Proof.
R: Ring
m, n: nat
r: R
M: Matrix R m n
matrix_transpose (matrix_lact r M) = matrix_lact r (matrix_transpose M)
  apply path_matrix.
R: Ring
m, n: nat
r: R
M: Matrix R m n
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < m)%nat),
entry (matrix_transpose (matrix_lact r M)) i j =
entry (matrix_lact r (matrix_transpose M)) i j
  intros i j Hi Hj.
R: Ring
m, n: nat
r: R
M: Matrix R m n
i, j: nat
Hi: (i < n)%nat
Hj: (j < m)%nat
entry (matrix_transpose (matrix_lact r M)) i j =
entry (matrix_lact r (matrix_transpose M)) i j
  by rewrite !entry_Build_Matrix, !entry_Build_Vector.
Defined.

(** The negation of a transposed matrix is the same as the transposed matrix of the negation. *)
Definition matrix_transpose_negate {R : Ring} {m n} (M : Matrix R m n)
  : matrix_transpose (matrix_negate M) = matrix_negate (matrix_transpose M).
R: Ring
m, n: nat
M: Matrix R m n
matrix_transpose (matrix_negate M) = matrix_negate (matrix_transpose M)
Proof.
R: Ring
m, n: nat
M: Matrix R m n
matrix_transpose (matrix_negate M) = matrix_negate (matrix_transpose M)
  apply path_matrix.
R: Ring
m, n: nat
M: Matrix R m n
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < m)%nat),
entry (matrix_transpose (matrix_negate M)) i j =
entry (matrix_negate (matrix_transpose M)) i j
  intros i j Hi Hj.
R: Ring
m, n: nat
M: Matrix R m n
i, j: nat
Hi: (i < n)%nat
Hj: (j < m)%nat
entry (matrix_transpose (matrix_negate M)) i j =
entry (matrix_negate (matrix_transpose M)) i j
  by rewrite !entry_Build_Matrix, !entry_Build_Vector.
Defined.

(** Transpose distributes over multiplication when you reverse the ring multiplication. *)
Definition matrix_transpose_mult {R : Ring} {m n p}
  (M : Matrix R m n) (N : Matrix R n p)
  : matrix_transpose (matrix_mult M N)
    = matrix_mult (R:=rng_op R) (matrix_transpose N) (matrix_transpose M).
R: Ring
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
matrix_transpose (matrix_mult M N) =
matrix_mult (matrix_transpose N) (matrix_transpose M)
Proof.
R: Ring
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
matrix_transpose (matrix_mult M N) =
matrix_mult (matrix_transpose N) (matrix_transpose M)
  apply path_matrix.
R: Ring
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
forall (i j : nat) (Hi : (i < p)%nat) (Hj : (j < m)%nat),
entry (matrix_transpose (matrix_mult M N)) i j =
entry (matrix_mult (matrix_transpose N) (matrix_transpose M)) i j
  intros i j Hi Hj.
R: Ring
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
i, j: nat
Hi: (i < p)%nat
Hj: (j < m)%nat
entry (matrix_transpose (matrix_mult M N)) i j =
entry (matrix_mult (matrix_transpose N) (matrix_transpose M)) i j
  rewrite 3 entry_Build_Matrix.
R: Ring
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
i, j: nat
Hi: (i < p)%nat
Hj: (j < m)%nat
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => entry M j k * entry N k i) =
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   entry (matrix_transpose N) i k * entry (matrix_transpose M) k j)
  apply path_ab_sum.
R: Ring
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
i, j: nat
Hi: (i < p)%nat
Hj: (j < m)%nat
forall (k : nat) (Hk : (k < n)%nat),
entry M j k * entry N k i =
entry (matrix_transpose N) i k * entry (matrix_transpose M) k j
  intros k Hk.
R: Ring
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
i, j: nat
Hi: (i < p)%nat
Hj: (j < m)%nat
k: nat
Hk: (k < n)%nat
entry M j k * entry N k i =
entry (matrix_transpose N) i k * entry (matrix_transpose M) k j
  rewrite 2 entry_Build_Matrix.
R: Ring
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
i, j: nat
Hi: (i < p)%nat
Hj: (j < m)%nat
k: nat
Hk: (k < n)%nat
entry M j k * entry N k i = entry N k i * entry M j k
  reflexivity.
Defined.

(** When the ring is commutative, there is no need to reverse the multiplication. *)
Definition matrix_transpose_mult_comm {R : CRing} {m n p}
  (M : Matrix R m n) (N : Matrix R n p)
  : matrix_transpose (matrix_mult M N)
    = matrix_mult (matrix_transpose N) (matrix_transpose M).
R: CRing
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
matrix_transpose (matrix_mult M N) =
matrix_mult (matrix_transpose N) (matrix_transpose M)
Proof.
R: CRing
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
matrix_transpose (matrix_mult M N) =
matrix_mult (matrix_transpose N) (matrix_transpose M)
  lhs napply matrix_transpose_mult.
R: CRing
m, n, p: nat
M: Matrix R m n
N: Matrix R n p
matrix_mult (matrix_transpose N) (matrix_transpose M) =
matrix_mult (matrix_transpose N) (matrix_transpose M)
  apply matrix_mult_rng_op.
Defined.

(** The transpose of the zero matrix is the zero matrix. *)
Definition matrix_transpose_zero {R : Ring} {m n}
  : matrix_transpose (matrix_zero R m n) = matrix_zero R n m.
R: Ring
m, n: nat
matrix_transpose (matrix_zero R m n) = matrix_zero R n m
Proof.
R: Ring
m, n: nat
matrix_transpose (matrix_zero R m n) = matrix_zero R n m
  apply path_matrix.
R: Ring
m, n: nat
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < m)%nat),
entry (matrix_transpose (matrix_zero R m n)) i j =
entry (matrix_zero R n m) i j
  intros i j Hi Hj.
R: Ring
m, n, i, j: nat
Hi: (i < n)%nat
Hj: (j < m)%nat
entry (matrix_transpose (matrix_zero R m n)) i j =
entry (matrix_zero R n m) i j
  by rewrite !entry_Build_Matrix.
Defined.

(** The transpose of the identity matrix is the identity matrix. *)
Definition matrix_transpose_identity@{i} {R : Ring@{i}} {n}
  : matrix_transpose (identity_matrix R n) = identity_matrix R n.
R: Ring
n: nat
matrix_transpose (identity_matrix R n) = identity_matrix R n
Proof.
R: Ring
n: nat
matrix_transpose (identity_matrix R n) = identity_matrix R n
  apply path_matrix.
R: Ring
n: nat
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
entry (matrix_transpose (identity_matrix R n)) i j =
entry (identity_matrix R n) i j
  intros i j Hi Hj.
R: Ring
n, i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
entry (matrix_transpose (identity_matrix R n)) i j =
entry (identity_matrix R n) i j
  rewrite 3 entry_Build_Matrix.
R: Ring
n, i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
kronecker_delta j i = kronecker_delta i j
  apply kronecker_delta_symm.
Defined.

(** ** Diagonal matrices *)

(** A diagonal matrix is a matrix with zeros everywhere except on the diagonal. Its entries are given by a vector. *)
Definition matrix_diag {R : Ring@{i}} {n : nat} (v : Vector R n)
  : Matrix R n n.
R: Ring
n: nat
v: Vector R n
Matrix R n n
Proof.
R: Ring
n: nat
v: Vector R n
Matrix R n n
  snapply Build_Matrix.
R: Ring
n: nat
v: Vector R n
forall i j : nat, (i < n)%nat -> (j < n)%nat -> R
  intros i j H1 H2.
R: Ring
n: nat
v: Vector R n
i, j: nat
H1: (i < n)%nat
H2: (j < n)%nat
R
  exact (kronecker_delta i j * Vector.entry v i).
Defined.

(** Addition of diagonal matrices is the same as addition of the corresponding vectors. *)
Definition matrix_diag_plus {R : Ring@{i}} {n : nat} (v w : Vector R n)
  : matrix_plus (matrix_diag v) (matrix_diag w) = matrix_diag (vector_plus v w).
R: Ring
n: nat
v, w: Vector R n
matrix_plus (matrix_diag v) (matrix_diag w) = matrix_diag (vector_plus v w)
Proof.
R: Ring
n: nat
v, w: Vector R n
matrix_plus (matrix_diag v) (matrix_diag w) = matrix_diag (vector_plus v w)
  symmetry.
R: Ring
n: nat
v, w: Vector R n
matrix_diag (vector_plus v w) = matrix_plus (matrix_diag v) (matrix_diag w)
  snapply path_matrix.
R: Ring
n: nat
v, w: Vector R n
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
entry (matrix_diag (vector_plus v w)) i j =
entry (matrix_plus (matrix_diag v) (matrix_diag w)) i j
  intros i j Hi Hj.
R: Ring
n: nat
v, w: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
entry (matrix_diag (vector_plus v w)) i j =
entry (matrix_plus (matrix_diag v) (matrix_diag w)) i j
  rewrite 2 entry_Build_Matrix, 5 entry_Build_Vector.
R: Ring
n: nat
v, w: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
kronecker_delta i j * (Vector.entry v i + Vector.entry w i) =
kronecker_delta i j * Vector.entry v i +
kronecker_delta i j * Vector.entry w i
  napply rng_dist_l.
Defined.

(** Matrix multiplication of diagonal matrices is the same as multiplying the corresponding vectors pointwise. *)
Definition matrix_diag_mult {R : Ring} {n : nat} (v w : Vector R n)
  : matrix_mult (matrix_diag v) (matrix_diag w)
    = matrix_diag (vector_map2 (.*.) v w).
R: Ring
n: nat
v, w: Vector R n
matrix_mult (matrix_diag v) (matrix_diag w) =
matrix_diag (vector_map2 mult v w)
Proof.
R: Ring
n: nat
v, w: Vector R n
matrix_mult (matrix_diag v) (matrix_diag w) =
matrix_diag (vector_map2 mult v w)
  snapply path_matrix.
R: Ring
n: nat
v, w: Vector R n
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
entry (matrix_mult (matrix_diag v) (matrix_diag w)) i j =
entry (matrix_diag (vector_map2 mult v w)) i j
  intros i j Hi Hj.
R: Ring
n: nat
v, w: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
entry (matrix_mult (matrix_diag v) (matrix_diag w)) i j =
entry (matrix_diag (vector_map2 mult v w)) i j
  rewrite 2 entry_Build_Matrix.
R: Ring
n: nat
v, w: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   entry (matrix_diag v) i k * entry (matrix_diag w) k j) =
kronecker_delta i j * Vector.entry (vector_map2 mult v w) i
  lhs snapply path_ab_sum.
R: Ring
n: nat
v, w: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
forall (k : nat) (Hk : (k < n)%nat),
entry (matrix_diag v) i k * entry (matrix_diag w) k j = ?Goal0 k Hk
R: Ring
n: nat
v, w: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
ab_sum n ?Goal0 = kronecker_delta i j * Vector.entry (vector_map2 mult v w) i
  {
R: Ring
n: nat
v, w: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
forall (k : nat) (Hk : (k < n)%nat),
entry (matrix_diag v) i k * entry (matrix_diag w) k j = ?Goal0 k Hk intros k Hk.
R: Ring
n: nat
v, w: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
k: nat
Hk: (k < n)%nat
entry (matrix_diag v) i k * entry (matrix_diag w) k j = ?Goal k Hk
    rewrite 2 entry_Build_Matrix.
R: Ring
n: nat
v, w: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
k: nat
Hk: (k < n)%nat
kronecker_delta i k * Vector.entry v i *
(kronecker_delta k j * Vector.entry w k) = ?Goal k Hk
    rewrite rng_mult_assoc.
R: Ring
n: nat
v, w: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
k: nat
Hk: (k < n)%nat
kronecker_delta i k * Vector.entry v i * kronecker_delta k j *
Vector.entry w k = ?Goal k Hk
    rewrite <- (rng_mult_assoc (kronecker_delta _ _)).
R: Ring
n: nat
v, w: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
k: nat
Hk: (k < n)%nat
kronecker_delta i k * (Vector.entry v i * kronecker_delta k j) *
Vector.entry w k = ?Goal k Hk
    rewrite kronecker_delta_comm.
R: Ring
n: nat
v, w: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
k: nat
Hk: (k < n)%nat
kronecker_delta i k * (kronecker_delta k j * Vector.entry v i) *
Vector.entry w k = ?Goal k Hk
    rewrite <- 2 rng_mult_assoc.
R: Ring
n: nat
v, w: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
k: nat
Hk: (k < n)%nat
kronecker_delta i k *
(kronecker_delta k j * (Vector.entry v i * Vector.entry w k)) = 
?Goal k Hk
    reflexivity. }
R: Ring
n: nat
v, w: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   kronecker_delta i k *
   (kronecker_delta k j * (Vector.entry v i * Vector.entry w k))) =
kronecker_delta i j * Vector.entry (vector_map2 mult v w) i
  rewrite (rng_sum_kronecker_delta_l _ _ Hi).
R: Ring
n: nat
v, w: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
kronecker_delta i j * (Vector.entry v i * Vector.entry w i) =
kronecker_delta i j * Vector.entry (vector_map2 mult v w) i
  by rewrite entry_Build_Vector.
Defined.

(** The transpose of a diagonal matrix is the same diagonal matrix. *)
Definition matrix_transpose_diag {R : Ring@{i}} {n : nat} (v : Vector R n)
  : matrix_transpose (matrix_diag v) = matrix_diag v.
R: Ring
n: nat
v: Vector R n
matrix_transpose (matrix_diag v) = matrix_diag v
Proof.
R: Ring
n: nat
v: Vector R n
matrix_transpose (matrix_diag v) = matrix_diag v
  snapply path_matrix.
R: Ring
n: nat
v: Vector R n
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
entry (matrix_transpose (matrix_diag v)) i j = entry (matrix_diag v) i j
  intros i j Hi Hj.
R: Ring
n: nat
v: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
entry (matrix_transpose (matrix_diag v)) i j = entry (matrix_diag v) i j
  rewrite 3 entry_Build_Matrix.
R: Ring
n: nat
v: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
kronecker_delta j i * Vector.entry v j =
kronecker_delta i j * Vector.entry v i
  rewrite kronecker_delta_symm.
R: Ring
n: nat
v: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
kronecker_delta i j * Vector.entry v j =
kronecker_delta i j * Vector.entry v i
  unfold kronecker_delta.
R: Ring
n: nat
v: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
(if dec (i = j) then 1 else 0) * Vector.entry v j =
(if dec (i = j) then 1 else 0) * Vector.entry v i
  destruct (dec (i = j)) as [p|np].
R: Ring
n: nat
v: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
p: i = j
1 * Vector.entry v j = 1 * Vector.entry v i
R: Ring
n: nat
v: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
np: i <> j
0 * Vector.entry v j = 0 * Vector.entry v i
  1: f_ap; symmetry; by apply path_entry_vector.
R: Ring
n: nat
v: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
np: i <> j
0 * Vector.entry v j = 0 * Vector.entry v i
  by rewrite !rng_mult_zero_l.
Defined.

(** The diagonal matrix construction is injective. *)
Instance isinj_matrix_diag {R : Ring@{i}} {n : nat}
  : IsInjective (@matrix_diag R n).
R: Ring
n: nat
IsInjective matrix_diag
Proof.
R: Ring
n: nat
IsInjective matrix_diag
  intros v1 v2 p.
R: Ring
n: nat
v1, v2: Vector R n
p: matrix_diag v1 = matrix_diag v2
v1 = v2
  snapply path_vector.
R: Ring
n: nat
v1, v2: Vector R n
p: matrix_diag v1 = matrix_diag v2
forall (i : nat) (H : (i < n)%nat), Vector.entry v1 i = Vector.entry v2 i
  intros i Hi.
R: Ring
n: nat
v1, v2: Vector R n
p: matrix_diag v1 = matrix_diag v2
i: nat
Hi: (i < n)%nat
Vector.entry v1 i = Vector.entry v2 i
  apply (ap (fun M => entry M i i)) in p.
R: Ring
n: nat
v1, v2: Vector R n
i: nat
Hi: (i < n)%nat
p: entry (matrix_diag v1) i i = entry (matrix_diag v2) i i
Vector.entry v1 i = Vector.entry v2 i
  rewrite 2 entry_Build_Matrix in p.
R: Ring
n: nat
v1, v2: Vector R n
i: nat
Hi: (i < n)%nat
p: kronecker_delta i i * Vector.entry v1 i =
kronecker_delta i i * Vector.entry v2 i
Vector.entry v1 i = Vector.entry v2 i
  rewrite kronecker_delta_refl in p.
R: Ring
n: nat
v1, v2: Vector R n
i: nat
Hi: (i < n)%nat
p: 1 * Vector.entry v1 i = 1 * Vector.entry v2 i
Vector.entry v1 i = Vector.entry v2 i
  by rewrite 2 rng_mult_one_l in p.
Defined.

(** A matrix is diagonal if it is equal to a diagonal matrix. *)
Class IsDiagonal@{i} {R : Ring@{i}} {n : nat} (M : Matrix R n n) : Type@{i} := {
  isdiagonal_diag_vector : Vector R n;
  isdiagonal_diag : M = matrix_diag isdiagonal_diag_vector;
}.

Arguments isdiagonal_diag_vector {R n} M {_}.
Arguments isdiagonal_diag {R n} M {_}.

Definition issig_IsDiagonal {R : Ring@{i}} {n : nat} {M : Matrix R n n}
  : _ <~> IsDiagonal M
  := ltac:(issig).

(** A matrix is diagonal in a unique way. *)
Instance ishprop_isdiagonal {R : Ring@{i}} {n : nat} (M : Matrix R n n)
  : IsHProp (IsDiagonal M).
R: Ring
n: nat
M: Matrix R n n
IsHProp (IsDiagonal M)
Proof.
R: Ring
n: nat
M: Matrix R n n
IsHProp (IsDiagonal M)
  snapply hprop_allpath.
R: Ring
n: nat
M: Matrix R n n
forall x y : IsDiagonal M, x = y
  intros x y.
R: Ring
n: nat
M: Matrix R n n
x, y: IsDiagonal M
x = y
  snapply ((equiv_ap' issig_IsDiagonal^-1%equiv _ _ )^-1%equiv).
R: Ring
n: nat
M: Matrix R n n
x, y: IsDiagonal M
issig_IsDiagonal^-1%equiv x = issig_IsDiagonal^-1%equiv y
  rapply path_sigma_hprop; cbn.
R: Ring
n: nat
M: Matrix R n n
x, y: IsDiagonal M
isdiagonal_diag_vector M = isdiagonal_diag_vector M
  apply isinj_matrix_diag.
R: Ring
n: nat
M: Matrix R n n
x, y: IsDiagonal M
matrix_diag (isdiagonal_diag_vector M) =
matrix_diag (isdiagonal_diag_vector M)
  exact ((isdiagonal_diag M)^ @ isdiagonal_diag M).
Defined.

(** The zero matrix is diagonal. *)
Instance isdiagonal_matrix_zero {R : Ring@{i}} {n : nat}
  : IsDiagonal (matrix_zero R n n).
R: Ring
n: nat
IsDiagonal (matrix_zero R n n)
Proof.
R: Ring
n: nat
IsDiagonal (matrix_zero R n n)
  exists (vector_zero R n).
R: Ring
n: nat
matrix_zero R n n = matrix_diag (vector_zero R n)
  snapply path_matrix.
R: Ring
n: nat
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
entry (matrix_zero R n n) i j = entry (matrix_diag (vector_zero R n)) i j
  intros i j Hi Hj.
R: Ring
n, i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
entry (matrix_zero R n n) i j = entry (matrix_diag (vector_zero R n)) i j
  rewrite 2 entry_Build_Matrix, entry_Build_Vector.
R: Ring
n, i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
0 = kronecker_delta i j * 0
  by rewrite rng_mult_zero_r.
Defined.

(** The identity matrix is diagonal. *)
Instance isdiagonal_identity_matrix {R : Ring@{i}} {n : nat}
  : IsDiagonal (identity_matrix R n).
R: Ring
n: nat
IsDiagonal (identity_matrix R n)
Proof.
R: Ring
n: nat
IsDiagonal (identity_matrix R n)
  exists (Build_Vector R n (fun _ _ => 1)).
R: Ring
n: nat
identity_matrix R n =
matrix_diag (Build_Vector R n (fun (i : nat) (_ : (i < n)%nat) => 1))
  snapply path_matrix.
R: Ring
n: nat
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
entry (identity_matrix R n) i j =
entry
  (matrix_diag (Build_Vector R n (fun (i0 : nat) (_ : (i0 < n)%nat) => 1))) i
  j
  intros i j Hi Hj.
R: Ring
n, i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
entry (identity_matrix R n) i j =
entry
  (matrix_diag (Build_Vector R n (fun (i0 : nat) (_ : (i0 < n)%nat) => 1))) i
  j
  rewrite 2 entry_Build_Matrix, entry_Build_Vector.
R: Ring
n, i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
kronecker_delta i j = kronecker_delta i j * 1
  by rewrite rng_mult_one_r.
Defined.

(** The sum of two diagonal matrices is diagonal. *)
Instance isdiagonal_matrix_plus {R : Ring@{i}} {n : nat}
  (M N : Matrix R n n) `{IsDiagonal R n M} `{IsDiagonal R n N}
  : IsDiagonal (matrix_plus M N).
R: Ring
n: nat
M, N: Matrix R n n
H: IsDiagonal M
H0: IsDiagonal N
IsDiagonal (matrix_plus M N)
Proof.
R: Ring
n: nat
M, N: Matrix R n n
H: IsDiagonal M
H0: IsDiagonal N
IsDiagonal (matrix_plus M N)
  exists (vector_plus (isdiagonal_diag_vector M) (isdiagonal_diag_vector N)).
R: Ring
n: nat
M, N: Matrix R n n
H: IsDiagonal M
H0: IsDiagonal N
matrix_plus M N =
matrix_diag
  (vector_plus (isdiagonal_diag_vector M) (isdiagonal_diag_vector N))
  rewrite (isdiagonal_diag M), (isdiagonal_diag N).
R: Ring
n: nat
M, N: Matrix R n n
H: IsDiagonal M
H0: IsDiagonal N
matrix_plus (matrix_diag (isdiagonal_diag_vector M))
  (matrix_diag (isdiagonal_diag_vector N)) =
matrix_diag
  (vector_plus (isdiagonal_diag_vector M) (isdiagonal_diag_vector N))
  apply matrix_diag_plus.
Defined.

(** The negative of a diagonal matrix is diagonal. *)
Instance isdiagonal_matrix_negate {R : Ring@{i}} {n : nat}
  (M : Matrix R n n) `{IsDiagonal R n M}
  : IsDiagonal (matrix_negate M).
R: Ring
n: nat
M: Matrix R n n
H: IsDiagonal M
IsDiagonal (matrix_negate M)
Proof.
R: Ring
n: nat
M: Matrix R n n
H: IsDiagonal M
IsDiagonal (matrix_negate M)
  exists (vector_neg _ _ (isdiagonal_diag_vector M)).
R: Ring
n: nat
M: Matrix R n n
H: IsDiagonal M
matrix_negate M = matrix_diag (vector_neg R n (isdiagonal_diag_vector M))
  rewrite (isdiagonal_diag M).
R: Ring
n: nat
M: Matrix R n n
H: IsDiagonal M
matrix_negate (matrix_diag (isdiagonal_diag_vector M)) =
matrix_diag (vector_neg R n (isdiagonal_diag_vector M))
  snapply path_matrix.
R: Ring
n: nat
M: Matrix R n n
H: IsDiagonal M
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
entry (matrix_negate (matrix_diag (isdiagonal_diag_vector M))) i j =
entry (matrix_diag (vector_neg R n (isdiagonal_diag_vector M))) i j
  intros i j Hi Hj.
R: Ring
n: nat
M: Matrix R n n
H: IsDiagonal M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
entry (matrix_negate (matrix_diag (isdiagonal_diag_vector M))) i j =
entry (matrix_diag (vector_neg R n (isdiagonal_diag_vector M))) i j
  rewrite !entry_Build_Matrix, !entry_Build_Vector.
R: Ring
n: nat
M: Matrix R n n
H: IsDiagonal M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
- (kronecker_delta i j * Vector.entry (isdiagonal_diag_vector M) i) =
kronecker_delta i j * - Vector.entry (isdiagonal_diag_vector M) i
  by rewrite rng_mult_negate_r.
Defined.

(** The product of two diagonal matrices is diagonal. *)
Instance isdiagonal_matrix_mult {R : Ring@{i}} {n : nat}
  (M N : Matrix R n n) `{IsDiagonal R n M} `{IsDiagonal R n N}
  : IsDiagonal (matrix_mult M N).
R: Ring
n: nat
M, N: Matrix R n n
H: IsDiagonal M
H0: IsDiagonal N
IsDiagonal (matrix_mult M N)
Proof.
R: Ring
n: nat
M, N: Matrix R n n
H: IsDiagonal M
H0: IsDiagonal N
IsDiagonal (matrix_mult M N)
  exists (vector_map2 (.*.) (isdiagonal_diag_vector M) (isdiagonal_diag_vector N)).
R: Ring
n: nat
M, N: Matrix R n n
H: IsDiagonal M
H0: IsDiagonal N
matrix_mult M N =
matrix_diag
  (vector_map2 mult (isdiagonal_diag_vector M) (isdiagonal_diag_vector N))
  rewrite (isdiagonal_diag M), (isdiagonal_diag N).
R: Ring
n: nat
M, N: Matrix R n n
H: IsDiagonal M
H0: IsDiagonal N
matrix_mult (matrix_diag (isdiagonal_diag_vector M))
  (matrix_diag (isdiagonal_diag_vector N)) =
matrix_diag
  (vector_map2 mult (isdiagonal_diag_vector M) (isdiagonal_diag_vector N))
  apply matrix_diag_mult.
Defined.

(** The transpose of a diagonal matrix is diagonal. *)
Instance isdiagonal_matrix_transpose {R : Ring@{i}} {n : nat}
  (M : Matrix R n n) `{IsDiagonal R n M}
  : IsDiagonal (matrix_transpose M).
R: Ring
n: nat
M: Matrix R n n
H: IsDiagonal M
IsDiagonal (matrix_transpose M)
Proof.
R: Ring
n: nat
M: Matrix R n n
H: IsDiagonal M
IsDiagonal (matrix_transpose M)
  exists (isdiagonal_diag_vector M).
R: Ring
n: nat
M: Matrix R n n
H: IsDiagonal M
matrix_transpose M = matrix_diag (isdiagonal_diag_vector M)
  rewrite (isdiagonal_diag M).
R: Ring
n: nat
M: Matrix R n n
H: IsDiagonal M
matrix_transpose (matrix_diag (isdiagonal_diag_vector M)) =
matrix_diag (isdiagonal_diag_vector M)
  apply matrix_transpose_diag.
Defined.

(** Given a square matrix, we can extract the diagonal as a vector. *)
Definition matrix_diag_vector {R : Ring} {n : nat} (M : Matrix R n n)
  : Vector R n
  := Build_Vector R n (fun i _ => entry M i i).

(** Diagonal matrices form a subring of the ring of square matrices. *)
Definition matrix_diag_ring@{i} (R : Ring@{i}) (n : nat)
  : Subring@{i i} (matrix_ring R n).
R: Ring
n: nat
Subring (matrix_ring R n)
Proof.
R: Ring
n: nat
Subring (matrix_ring R n)
  snapply (Build_Subring' (fun M : matrix_ring R n => IsDiagonal M) _); hnf.
R: Ring
n: nat
forall x : matrix_ring R n, IsHProp (IsDiagonal x)
R: Ring
n: nat
forall x y : matrix_ring R n,
IsDiagonal x -> IsDiagonal y -> IsDiagonal (x - y)
R: Ring
n: nat
forall x y : matrix_ring R n,
IsDiagonal x -> IsDiagonal y -> IsDiagonal (x * y)
R: Ring
n: nat
IsDiagonal 1
  -
R: Ring
n: nat
forall x : matrix_ring R n, IsHProp (IsDiagonal x) intros; exact _.
  -
R: Ring
n: nat
forall x y : matrix_ring R n,
IsDiagonal x -> IsDiagonal y -> IsDiagonal (x - y) intros x y dx dy.
R: Ring
n: nat
x, y: matrix_ring R n
dx: IsDiagonal x
dy: IsDiagonal y
IsDiagonal (x - y)
    napply isdiagonal_matrix_plus; trivial.
R: Ring
n: nat
x, y: matrix_ring R n
dx: IsDiagonal x
dy: IsDiagonal y
IsDiagonal (- y)
    by napply isdiagonal_matrix_negate.
  -
R: Ring
n: nat
forall x y : matrix_ring R n,
IsDiagonal x -> IsDiagonal y -> IsDiagonal (x * y) napply isdiagonal_matrix_mult.
  -
R: Ring
n: nat
IsDiagonal 1 napply isdiagonal_identity_matrix.
Defined.

(** ** Trace *)

(** The trace of a square matrix is the sum of the diagonal entries. *)
Definition matrix_trace {R : Ring} {n} (M : Matrix R n n) : R
  := ab_sum n (fun i Hi => entry M i i).

(** The trace of a matrix preserves addition. *)
Definition matrix_trace_plus {R : Ring} {n} (M N : Matrix R n n)
  : matrix_trace (matrix_plus M N) = (matrix_trace M) + (matrix_trace N).
R: Ring
n: nat
M, N: Matrix R n n
matrix_trace (matrix_plus M N) = matrix_trace M + matrix_trace N
Proof.
R: Ring
n: nat
M, N: Matrix R n n
matrix_trace (matrix_plus M N) = matrix_trace M + matrix_trace N
  unfold matrix_trace.
R: Ring
n: nat
M, N: Matrix R n n
ab_sum n (fun (i : nat) (Hi : (i < n)%nat) => entry (matrix_plus M N) i i) =
ab_sum n (fun (i : nat) (Hi : (i < n)%nat) => entry M i i) +
ab_sum n (fun (i : nat) (Hi : (i < n)%nat) => entry N i i)
  lhs napply path_ab_sum.
R: Ring
n: nat
M, N: Matrix R n n
forall (k : nat) (Hk : (k < n)%nat), entry (matrix_plus M N) k k = ?Goal k Hk
R: Ring
n: nat
M, N: Matrix R n n
ab_sum n ?Goal =
ab_sum n (fun (i : nat) (Hi : (i < n)%nat) => entry M i i) +
ab_sum n (fun (i : nat) (Hi : (i < n)%nat) => entry N i i)
  {
R: Ring
n: nat
M, N: Matrix R n n
forall (k : nat) (Hk : (k < n)%nat), entry (matrix_plus M N) k k = ?Goal k Hk intros i Hi.
R: Ring
n: nat
M, N: Matrix R n n
i: nat
Hi: (i < n)%nat
entry (matrix_plus M N) i i = ?Goal i Hi
    by rewrite entry_Build_Matrix. }
R: Ring
n: nat
M, N: Matrix R n n
ab_sum n
  (fun (i : nat) (Hi : (i < n)%nat) =>
   Vector.entry (Vector.entry M i) i + Vector.entry (Vector.entry N i) i) =
ab_sum n (fun (i : nat) (Hi : (i < n)%nat) => entry M i i) +
ab_sum n (fun (i : nat) (Hi : (i < n)%nat) => entry N i i)
  by rewrite ab_sum_plus.
Defined.

(** The trace of a matrix preserves scalar multiplication. *)
Definition matrix_trace_lact {R : Ring} {n} (r : R) (M : Matrix R n n)
  : matrix_trace (matrix_lact r M) = r * matrix_trace M.
R: Ring
n: nat
r: R
M: Matrix R n n
matrix_trace (matrix_lact r M) = r * matrix_trace M
Proof.
R: Ring
n: nat
r: R
M: Matrix R n n
matrix_trace (matrix_lact r M) = r * matrix_trace M
  unfold matrix_trace.
R: Ring
n: nat
r: R
M: Matrix R n n
ab_sum n (fun (i : nat) (Hi : (i < n)%nat) => entry (matrix_lact r M) i i) =
r * ab_sum n (fun (i : nat) (Hi : (i < n)%nat) => entry M i i)
  rewrite rng_sum_dist_l.
R: Ring
n: nat
r: R
M: Matrix R n n
ab_sum n (fun (i : nat) (Hi : (i < n)%nat) => entry (matrix_lact r M) i i) =
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => r * entry M k k)
  apply path_ab_sum.
R: Ring
n: nat
r: R
M: Matrix R n n
forall (k : nat) (Hk : (k < n)%nat),
entry (matrix_lact r M) k k = r * entry M k k
  intros i Hi.
R: Ring
n: nat
r: R
M: Matrix R n n
i: nat
Hi: (i < n)%nat
entry (matrix_lact r M) i i = r * entry M i i
  by rewrite entry_Build_Matrix.
Defined.

(** The trace of a matrix multiplication is the same as the trace of the reverse multiplication. This holds only in a commutative ring. *)
Definition matrix_trace_mult {R : CRing} {m n : nat}
  (M : Matrix R m n) (N : Matrix R n m)
  : matrix_trace (matrix_mult M N) = matrix_trace (matrix_mult N M).
R: CRing
m, n: nat
M: Matrix R m n
N: Matrix R n m
matrix_trace (matrix_mult M N) = matrix_trace (matrix_mult N M)
Proof.
R: CRing
m, n: nat
M: Matrix R m n
N: Matrix R n m
matrix_trace (matrix_mult M N) = matrix_trace (matrix_mult N M)
  lhs napply path_ab_sum.
R: CRing
m, n: nat
M: Matrix R m n
N: Matrix R n m
forall (k : nat) (Hk : (k < m)%nat), entry (matrix_mult M N) k k = ?Goal k Hk
R: CRing
m, n: nat
M: Matrix R m n
N: Matrix R n m
ab_sum m ?Goal = matrix_trace (matrix_mult N M)
  {
R: CRing
m, n: nat
M: Matrix R m n
N: Matrix R n m
forall (k : nat) (Hk : (k < m)%nat), entry (matrix_mult M N) k k = ?Goal k Hk intros i Hi.
R: CRing
m, n: nat
M: Matrix R m n
N: Matrix R n m
i: nat
Hi: (i < m)%nat
entry (matrix_mult M N) i i = ?Goal i Hi
    lhs napply entry_Build_Matrix.
R: CRing
m, n: nat
M: Matrix R m n
N: Matrix R n m
i: nat
Hi: (i < m)%nat
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => entry M i k * entry N k i) =
?Goal i Hi
    napply path_ab_sum.
R: CRing
m, n: nat
M: Matrix R m n
N: Matrix R n m
i: nat
Hi: (i < m)%nat
forall (k : nat) (Hk : (k < n)%nat), entry M i k * entry N k i = ?Goal0 k Hk
    intros j Hj.
R: CRing
m, n: nat
M: Matrix R m n
N: Matrix R n m
i: nat
Hi: (i < m)%nat
j: nat
Hj: (j < n)%nat
entry M i j * entry N j i = ?Goal0 j Hj
    apply rng_mult_comm. }
R: CRing
m, n: nat
M: Matrix R m n
N: Matrix R n m
ab_sum m
  (fun (i : nat) (Hi : (i < m)%nat) =>
   ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => entry N j i * entry M i j)) =
matrix_trace (matrix_mult N M)
  lhs napply ab_sum_sum.
R: CRing
m, n: nat
M: Matrix R m n
N: Matrix R n m
ab_sum n
  (fun (j : nat) (Hj : (j < n)%nat) =>
   ab_sum m (fun (i : nat) (Hi : (i < m)%nat) => entry N j i * entry M i j)) =
matrix_trace (matrix_mult N M)
  apply path_ab_sum.
R: CRing
m, n: nat
M: Matrix R m n
N: Matrix R n m
forall (k : nat) (Hk : (k < n)%nat),
ab_sum m (fun (i : nat) (Hi : (i < m)%nat) => entry N k i * entry M i k) =
entry (matrix_mult N M) k k
  intros i Hi.
R: CRing
m, n: nat
M: Matrix R m n
N: Matrix R n m
i: nat
Hi: (i < n)%nat
ab_sum m (fun (i0 : nat) (Hi0 : (i0 < m)%nat) => entry N i i0 * entry M i0 i) =
entry (matrix_mult N M) i i
  rhs napply entry_Build_Matrix.
R: CRing
m, n: nat
M: Matrix R m n
N: Matrix R n m
i: nat
Hi: (i < n)%nat
ab_sum m (fun (i0 : nat) (Hi0 : (i0 < m)%nat) => entry N i i0 * entry M i0 i) =
ab_sum m (fun (k : nat) (Hk : (k < m)%nat) => entry N i k * entry M k i)
  reflexivity.
Defined.

(** The trace of the transpose of a matrix is the same as the trace of the matrix. *)
Definition trace_transpose {R : Ring} {n} (M : Matrix R n n)
  : matrix_trace (matrix_transpose M) = matrix_trace M.
R: Ring
n: nat
M: Matrix R n n
matrix_trace (matrix_transpose M) = matrix_trace M
Proof.
R: Ring
n: nat
M: Matrix R n n
matrix_trace (matrix_transpose M) = matrix_trace M
  apply path_ab_sum.
R: Ring
n: nat
M: Matrix R n n
forall (k : nat) (Hk : (k < n)%nat),
entry (matrix_transpose M) k k = entry M k k
  intros i Hi.
R: Ring
n: nat
M: Matrix R n n
i: nat
Hi: (i < n)%nat
entry (matrix_transpose M) i i = entry M i i
  napply entry_Build_Matrix.
Defined.

(** ** Matrix minors *)

Definition skip (n : nat) : nat -> nat
  := fun i => if dec (i < n)%nat then i else i.+1%nat.

Instance isinjective_skip n : IsInjective (skip n).
n: nat
IsInjective (skip n)
Proof.
n: nat
IsInjective (skip n)
  hnf.
n: nat
forall x y : nat, skip n x = skip n y -> x = y
  intros x y p.
n, x, y: nat
p: skip n x = skip n y
x = y
  unfold skip in p.
n, x, y: nat
p: (if dec (x < n)%nat then x else x.+1%nat) =
(if dec (y < n)%nat then y else y.+1%nat)
x = y
  destruct (dec (x < n)%nat) as [H|H], (dec (y < n)%nat) as [H'|H'].
n, x, y: nat
H: (x < n)%nat
H': (y < n)%nat
p: x = y
x = y
n, x, y: nat
H: (x < n)%nat
H': ~ (y < n)%nat
p: x = y.+1%nat
x = y
n, x, y: nat
H: ~ (x < n)%nat
H': (y < n)%nat
p: x.+1%nat = y
x = y
n, x, y: nat
H: ~ (x < n)%nat
H': ~ (y < n)%nat
p: x.+1%nat = y.+1%nat
x = y
  -
n, x, y: nat
H: (x < n)%nat
H': (y < n)%nat
p: x = y
x = y exact p.
  -
n, x, y: nat
H: (x < n)%nat
H': ~ (y < n)%nat
p: x = y.+1%nat
x = y symmetry in p; destruct p.
n, y: nat
H: (y.+1 < n)%nat
H': ~ (y < n)%nat
y.+1%nat = y
    contradiction (H' (leq_trans _ H)).
  -
n, x, y: nat
H: ~ (x < n)%nat
H': (y < n)%nat
p: x.+1%nat = y
x = y destruct p.
n, x: nat
H: ~ (x < n)%nat
H': (x.+1 < n)%nat
x = x.+1%nat
    contradiction (H (leq_trans _ H')).
  -
n, x, y: nat
H: ~ (x < n)%nat
H': ~ (y < n)%nat
p: x.+1%nat = y.+1%nat
x = y by apply path_nat_succ.
Defined.

Local Instance lt_n1_skip k i n (H : (i < n.+1)%nat) (H' : (k < n)%nat)
  : (skip i k < n.+1)%nat.
k, i, n: nat
H: (i < n.+1)%nat
H': (k < n)%nat
(skip i k < n.+1)%nat
Proof.
k, i, n: nat
H: (i < n.+1)%nat
H': (k < n)%nat
(skip i k < n.+1)%nat
  unfold skip.
k, i, n: nat
H: (i < n.+1)%nat
H': (k < n)%nat
((if dec (k < i) then k else k.+1) < n.+1)%nat
  destruct (dec (k < i))%nat as [H''|H'']; exact _.
Defined.

Definition matrix_minor {R : Ring@{i}} {n : nat} (i j : nat)
  {Hi : (i < n.+1)%nat} {Hj : (j < n.+1)%nat} (M : Matrix R n.+1 n.+1)
  : Matrix R n n
  := Build_Matrix R n n (fun k l _ _ => entry M (skip i k) (skip j l)).

(** A minor of the zero matrix is again the zero matrix. *)
Definition matrix_minor_zero {R : Ring@{i}} {n : nat} (i j : nat)
  (Hi : (i < n.+1)%nat) (Hj : (j < n.+1)%nat)
  : matrix_minor i j (matrix_zero R n.+1 n.+1) = matrix_zero R n n.
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
matrix_minor i j (matrix_zero R n.+1 n.+1) = matrix_zero R n n
Proof.
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
matrix_minor i j (matrix_zero R n.+1 n.+1) = matrix_zero R n n
  apply path_matrix.
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
entry (matrix_minor i j (matrix_zero R n.+1 n.+1)) i0 j0 =
entry (matrix_zero R n n) i0 j0
  intros k l Hk Hl.
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
k, l: nat
Hk: (k < n)%nat
Hl: (l < n)%nat
entry (matrix_minor i j (matrix_zero R n.+1 n.+1)) k l =
entry (matrix_zero R n n) k l
  by rewrite !entry_Build_Matrix.
Defined.

Definition matrix_minor_identity {R : Ring@{i}} {n : nat}
  (i : nat) (Hi : (i < n.+1)%nat)
  : matrix_minor i i (identity_matrix R n.+1) = identity_matrix R n.
R: Ring
n, i: nat
Hi: (i < n.+1)%nat
matrix_minor i i (identity_matrix R n.+1) = identity_matrix R n
Proof.
R: Ring
n, i: nat
Hi: (i < n.+1)%nat
matrix_minor i i (identity_matrix R n.+1) = identity_matrix R n
  apply path_matrix.
R: Ring
n, i: nat
Hi: (i < n.+1)%nat
forall (i0 j : nat) (Hi0 : (i0 < n)%nat) (Hj : (j < n)%nat),
entry (matrix_minor i i (identity_matrix R n.+1)) i0 j =
entry (identity_matrix R n) i0 j
  intros j k Hj Hk.
R: Ring
n, i: nat
Hi: (i < n.+1)%nat
j, k: nat
Hj: (j < n)%nat
Hk: (k < n)%nat
entry (matrix_minor i i (identity_matrix R n.+1)) j k =
entry (identity_matrix R n) j k
  rewrite 3 entry_Build_Matrix.
R: Ring
n, i: nat
Hi: (i < n.+1)%nat
j, k: nat
Hj: (j < n)%nat
Hk: (k < n)%nat
kronecker_delta (skip i j) (skip i k) = kronecker_delta j k
  rapply kronecker_delta_map_inj.
Defined.

Definition matrix_minor_plus {R : Ring@{i}} {n : nat} (i j : nat)
  (Hi : (i < n.+1)%nat) (Hj : (j < n.+1)%nat) (M N : Matrix R n.+1 n.+1)
  : matrix_minor i j (matrix_plus M N)
    = matrix_plus (matrix_minor i j M) (matrix_minor i j N).
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
M, N: Matrix R n.+1 n.+1
matrix_minor i j (matrix_plus M N) =
matrix_plus (matrix_minor i j M) (matrix_minor i j N)
Proof.
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
M, N: Matrix R n.+1 n.+1
matrix_minor i j (matrix_plus M N) =
matrix_plus (matrix_minor i j M) (matrix_minor i j N)
  apply path_matrix.
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
M, N: Matrix R n.+1 n.+1
forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
entry (matrix_minor i j (matrix_plus M N)) i0 j0 =
entry (matrix_plus (matrix_minor i j M) (matrix_minor i j N)) i0 j0
  intros k l Hk Hl.
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
M, N: Matrix R n.+1 n.+1
k, l: nat
Hk: (k < n)%nat
Hl: (l < n)%nat
entry (matrix_minor i j (matrix_plus M N)) k l =
entry (matrix_plus (matrix_minor i j M) (matrix_minor i j N)) k l
  by rewrite !entry_Build_Matrix, !entry_Build_Vector.
Defined.

Definition matrix_minor_scale {R : Ring@{i}} {n : nat} (i j : nat)
  (Hi : (i < n.+1)%nat) (Hj : (j < n.+1)%nat) (r : R) (M : Matrix R n.+1 n.+1)
  : matrix_minor i j (matrix_lact r M) = matrix_lact r (matrix_minor i j M).
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
r: R
M: Matrix R n.+1 n.+1
matrix_minor i j (matrix_lact r M) = matrix_lact r (matrix_minor i j M)
Proof.
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
r: R
M: Matrix R n.+1 n.+1
matrix_minor i j (matrix_lact r M) = matrix_lact r (matrix_minor i j M)
  apply path_matrix.
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
r: R
M: Matrix R n.+1 n.+1
forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
entry (matrix_minor i j (matrix_lact r M)) i0 j0 =
entry (matrix_lact r (matrix_minor i j M)) i0 j0
  intros k l Hk Hl.
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
r: R
M: Matrix R n.+1 n.+1
k, l: nat
Hk: (k < n)%nat
Hl: (l < n)%nat
entry (matrix_minor i j (matrix_lact r M)) k l =
entry (matrix_lact r (matrix_minor i j M)) k l
  by rewrite !entry_Build_Matrix, !entry_Build_Vector.
Defined.

Definition matrix_minor_transpose {R : Ring@{i}} {n : nat} (i j : nat)
  (Hi : (i < n.+1)%nat) (Hj : (j < n.+1)%nat) (M : Matrix R n.+1 n.+1)
  : matrix_minor j i (matrix_transpose M)
    = matrix_transpose (matrix_minor i j M).
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
M: Matrix R n.+1 n.+1
matrix_minor j i (matrix_transpose M) = matrix_transpose (matrix_minor i j M)
Proof.
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
M: Matrix R n.+1 n.+1
matrix_minor j i (matrix_transpose M) = matrix_transpose (matrix_minor i j M)
  apply path_matrix.
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
M: Matrix R n.+1 n.+1
forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
entry (matrix_minor j i (matrix_transpose M)) i0 j0 =
entry (matrix_transpose (matrix_minor i j M)) i0 j0
  intros k l Hk Hl.
R: Ring
n, i, j: nat
Hi: (i < n.+1)%nat
Hj: (j < n.+1)%nat
M: Matrix R n.+1 n.+1
k, l: nat
Hk: (k < n)%nat
Hl: (l < n)%nat
entry (matrix_minor j i (matrix_transpose M)) k l =
entry (matrix_transpose (matrix_minor i j M)) k l
  by rewrite 4 entry_Build_Matrix.
Defined.

(** ** Triangular matrices *)

(** A matrix is upper triangular if all the entries below the diagonal are zero. *)
Class IsUpperTriangular@{i} {R : Ring@{i}} {n : nat} (M : Matrix@{i} R n n) : Type@{i}
  := upper_triangular
  : merely@{i} (forall i j (Hi : (i < n)%nat) (Hj : (j < n)%nat), (i < j)%nat -> entry M i j = 0).

Instance ishprop_isuppertriangular@{i} {R : Ring@{i}} {n : nat} (M : Matrix R n n)
  : IsHProp (IsUpperTriangular M).
R: Ring
n: nat
M: Matrix R n n
IsHProp (IsUpperTriangular M)
Proof.
R: Ring
n: nat
M: Matrix R n n
IsHProp (IsUpperTriangular M)
  apply istrunc_truncation@{i}.
Defined.

(** A matrix is lower triangular if all the entries above the diagonal are zero. We define it as the transpose being upper triangular. *)
Class IsLowerTriangular {R : Ring@{i}} {n : nat} (M : Matrix@{i} R n n) : Type@{i}
  := upper_triangular_transpose :: IsUpperTriangular (matrix_transpose M).

Instance ishprop_islowertriangular@{i} {R : Ring@{i}} {n : nat}
  (M : Matrix R n n)
  : IsHProp (IsLowerTriangular M).
R: Ring
n: nat
M: Matrix R n n
IsHProp (IsLowerTriangular M)
Proof.
R: Ring
n: nat
M: Matrix R n n
IsHProp (IsLowerTriangular M)
  apply istrunc_truncation@{i}.
Defined.

(** The transpose of a matrix is lower triangular if and only if the matrix is upper triangular. *)
Instance lower_triangular_transpose {R : Ring@{i}} {n : nat}
  (M : Matrix R n n) `{!IsUpperTriangular M}
  : IsLowerTriangular (matrix_transpose M).
R: Ring
n: nat
M: Matrix R n n
IsUpperTriangular0: IsUpperTriangular M
IsLowerTriangular (matrix_transpose M)
Proof.
R: Ring
n: nat
M: Matrix R n n
IsUpperTriangular0: IsUpperTriangular M
IsLowerTriangular (matrix_transpose M)
  unfold IsLowerTriangular.
R: Ring
n: nat
M: Matrix R n n
IsUpperTriangular0: IsUpperTriangular M
IsUpperTriangular (matrix_transpose (matrix_transpose M))
  by rewrite matrix_transpose_transpose.
Defined.

(** The sum of two upper triangular matrices is upper triangular. *)
Instance upper_triangular_plus@{i} {R : Ring@{i}} {n : nat} (M N : Matrix R n n)
  {H1 : IsUpperTriangular M} {H2 : IsUpperTriangular N}
  : IsUpperTriangular (matrix_plus M N).
R: Ring
n: nat
M, N: Matrix R n n
H1: IsUpperTriangular M
H2: IsUpperTriangular N
IsUpperTriangular (matrix_plus M N)
Proof.
R: Ring
n: nat
M, N: Matrix R n n
H1: IsUpperTriangular M
H2: IsUpperTriangular N
IsUpperTriangular (matrix_plus M N)
  unfold IsUpperTriangular.
R: Ring
n: nat
M, N: Matrix R n n
H1: IsUpperTriangular M
H2: IsUpperTriangular N
merely
  (forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
   (i < j)%nat -> entry (matrix_plus M N) i j = 0)
  (* We use [strip_reflections] rather than [strip_truncations] here and below because it generates fewer universe variables in some versions of Coq. *)
  strip_reflections; apply tr.
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
(i < j)%nat -> entry N i j = 0
H1: forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
(i < j)%nat -> entry M i j = 0
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
(i < j)%nat -> entry (matrix_plus M N) i j = 0
  intros i j Hi Hj lt_i_j.
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
entry (matrix_plus M N) i j = 0
  specialize (H1 i j Hi Hj lt_i_j).
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H1: entry M i j = 0
lt_i_j: (i < j)%nat
entry (matrix_plus M N) i j = 0
  specialize (H2 i j Hi Hj lt_i_j).
R: Ring
n: nat
M, N: Matrix R n n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H2: entry N i j = 0
H1: entry M i j = 0
lt_i_j: (i < j)%nat
entry (matrix_plus M N) i j = 0
  rewrite entry_Build_Matrix.
R: Ring
n: nat
M, N: Matrix R n n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H2: entry N i j = 0
H1: entry M i j = 0
lt_i_j: (i < j)%nat
Vector.entry (Vector.entry M i) j + Vector.entry (Vector.entry N i) j = 0
  change (Vector.entry (Vector.entry ?M ?i) ?j) with (entry M i j).
R: Ring
n: nat
M, N: Matrix R n n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H2: entry N i j = 0
H1: entry M i j = 0
lt_i_j: (i < j)%nat
entry M i j + entry N i j = 0
  rewrite H1, H2.
R: Ring
n: nat
M, N: Matrix R n n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H2: entry N i j = 0
H1: entry M i j = 0
lt_i_j: (i < j)%nat
0 + 0 = 0
  by rewrite rng_plus_zero_l.
Defined.

(** The sum of two lower triangular matrices is lower triangular. *)
Instance lower_triangular_plus {R : Ring@{i}} {n : nat}
  (M N : Matrix R n n) `{!IsLowerTriangular M} `{!IsLowerTriangular N}
  : IsLowerTriangular (matrix_plus M N).
R: Ring
n: nat
M, N: Matrix R n n
IsLowerTriangular0: IsLowerTriangular M
IsLowerTriangular1: IsLowerTriangular N
IsLowerTriangular (matrix_plus M N)
Proof.
R: Ring
n: nat
M, N: Matrix R n n
IsLowerTriangular0: IsLowerTriangular M
IsLowerTriangular1: IsLowerTriangular N
IsLowerTriangular (matrix_plus M N)
  unfold IsLowerTriangular.
R: Ring
n: nat
M, N: Matrix R n n
IsLowerTriangular0: IsLowerTriangular M
IsLowerTriangular1: IsLowerTriangular N
IsUpperTriangular (matrix_transpose (matrix_plus M N))
  rewrite matrix_transpose_plus.
R: Ring
n: nat
M, N: Matrix R n n
IsLowerTriangular0: IsLowerTriangular M
IsLowerTriangular1: IsLowerTriangular N
IsUpperTriangular (matrix_plus (matrix_transpose M) (matrix_transpose N))
  by apply upper_triangular_plus.
Defined.

(** The negation of an upper triangular matrix is upper triangular. *)
Instance upper_triangular_negate@{i} {R : Ring@{i}} {n : nat} (M : Matrix R n n)
  {H : IsUpperTriangular M}
  : IsUpperTriangular (matrix_negate M).
R: Ring
n: nat
M: Matrix R n n
H: IsUpperTriangular M
IsUpperTriangular (matrix_negate M)
Proof.
R: Ring
n: nat
M: Matrix R n n
H: IsUpperTriangular M
IsUpperTriangular (matrix_negate M)
  unfold IsUpperTriangular.
R: Ring
n: nat
M: Matrix R n n
H: IsUpperTriangular M
merely
  (forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
   (i < j)%nat -> entry (matrix_negate M) i j = 0)
  strip_reflections; apply tr.
R: Ring
n: nat
M: Matrix R n n
H: forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
(i < j)%nat -> entry M i j = 0
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
(i < j)%nat -> entry (matrix_negate M) i j = 0
  intros i j Hi Hj lt_i_j.
R: Ring
n: nat
M: Matrix R n n
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
entry (matrix_negate M) i j = 0
  rewrite entry_Build_Matrix.
R: Ring
n: nat
M: Matrix R n n
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
- Vector.entry (Vector.entry M i) j = 0
  rewrite <- rng_negate_zero; f_ap.
R: Ring
n: nat
M: Matrix R n n
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
Vector.entry (Vector.entry M i) j = 0
  by napply H.
Defined.

(** The negation of a lower triangular matrix is lower triangular. *)
Instance lower_triangular_negate {R : Ring@{i}} {n : nat}
  (M : Matrix R n n) `{!IsLowerTriangular M}
  : IsLowerTriangular (matrix_negate M).
R: Ring
n: nat
M: Matrix R n n
IsLowerTriangular0: IsLowerTriangular M
IsLowerTriangular (matrix_negate M)
Proof.
R: Ring
n: nat
M: Matrix R n n
IsLowerTriangular0: IsLowerTriangular M
IsLowerTriangular (matrix_negate M)
  unfold IsLowerTriangular.
R: Ring
n: nat
M: Matrix R n n
IsLowerTriangular0: IsLowerTriangular M
IsUpperTriangular (matrix_transpose (matrix_negate M))
  rewrite matrix_transpose_negate.
R: Ring
n: nat
M: Matrix R n n
IsLowerTriangular0: IsLowerTriangular M
IsUpperTriangular (matrix_negate (matrix_transpose M))
  by apply upper_triangular_negate.
Defined.

(** The product of two upper triangular matrices is upper triangular. *)
Instance upper_triangular_mult@{i} {R : Ring@{i}} {n : nat}
  (M N : Matrix R n n) {H1 : IsUpperTriangular M} {H2 : IsUpperTriangular N}
  : IsUpperTriangular (matrix_mult M N).
R: Ring
n: nat
M, N: Matrix R n n
H1: IsUpperTriangular M
H2: IsUpperTriangular N
IsUpperTriangular (matrix_mult M N)
Proof.
R: Ring
n: nat
M, N: Matrix R n n
H1: IsUpperTriangular M
H2: IsUpperTriangular N
IsUpperTriangular (matrix_mult M N)
  unfold IsUpperTriangular.
R: Ring
n: nat
M, N: Matrix R n n
H1: IsUpperTriangular M
H2: IsUpperTriangular N
merely
  (forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
   (i < j)%nat -> entry (matrix_mult M N) i j = 0)
  strip_reflections; apply tr.
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
(i < j)%nat -> entry N i j = 0
H1: forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
(i < j)%nat -> entry M i j = 0
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
(i < j)%nat -> entry (matrix_mult M N) i j = 0
  intros i j Hi Hj lt_i_j.
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
entry (matrix_mult M N) i j = 0
  rewrite entry_Build_Matrix.
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
ab_sum n (fun (k : nat) (Hk : (k < n)%nat) => entry M i k * entry N k j) = 0
  apply ab_sum_zero.
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
forall (k : nat) (Hk : (k < n)%nat), entry M i k * entry N k j = mon_unit
  intros k Hk.
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
k: nat
Hk: (k < n)%nat
entry M i k * entry N k j = mon_unit
  destruct (dec (k <= i)%nat) as [leq_k_i|gt_k_i].
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
k: nat
Hk: (k < n)%nat
leq_k_i: (k <= i)%nat
entry M i k * entry N k j = mon_unit
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
k: nat
Hk: (k < n)%nat
gt_k_i: ~ (k <= i)%nat
entry M i k * entry N k j = mon_unit
  {
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
k: nat
Hk: (k < n)%nat
leq_k_i: (k <= i)%nat
entry M i k * entry N k j = mon_unit rewrite H2.
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
k: nat
Hk: (k < n)%nat
leq_k_i: (k <= i)%nat
entry M i k * 0 = mon_unit
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
k: nat
Hk: (k < n)%nat
leq_k_i: (k <= i)%nat
(k < j)%nat
    1: by rewrite rng_mult_zero_r.
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
k: nat
Hk: (k < n)%nat
leq_k_i: (k <= i)%nat
(k < j)%nat
    rapply lt_leq_lt_trans. }
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
k: nat
Hk: (k < n)%nat
gt_k_i: ~ (k <= i)%nat
entry M i k * entry N k j = mon_unit
  apply gt_iff_not_leq in gt_k_i.
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
k: nat
Hk: (k < n)%nat
gt_k_i: (k > i)%nat
entry M i k * entry N k j = mon_unit
  rewrite H1.
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
k: nat
Hk: (k < n)%nat
gt_k_i: (k > i)%nat
0 * entry N k j = mon_unit
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
k: nat
Hk: (k < n)%nat
gt_k_i: (k > i)%nat
(i < k)%nat
  1: by rewrite rng_mult_zero_l.
R: Ring
n: nat
M, N: Matrix R n n
H2: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry N i0 j0 = 0
H1: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
k: nat
Hk: (k < n)%nat
gt_k_i: (k > i)%nat
(i < k)%nat
  assumption.
Defined.

(** The product of two lower triangular matrices is lower triangular. *)
Instance lower_triangular_mult {R : Ring@{i}} {n : nat}
  (M N : Matrix R n n) {H1 : IsLowerTriangular M} {H2 : IsLowerTriangular N}
  : IsLowerTriangular (matrix_mult M N).
R: Ring
n: nat
M, N: Matrix R n n
H1: IsLowerTriangular M
H2: IsLowerTriangular N
IsLowerTriangular (matrix_mult M N)
Proof.
R: Ring
n: nat
M, N: Matrix R n n
H1: IsLowerTriangular M
H2: IsLowerTriangular N
IsLowerTriangular (matrix_mult M N)
  unfold IsLowerTriangular.
R: Ring
n: nat
M, N: Matrix R n n
H1: IsLowerTriangular M
H2: IsLowerTriangular N
IsUpperTriangular (matrix_transpose (matrix_mult M N))
  rewrite matrix_transpose_mult.
R: Ring
n: nat
M, N: Matrix R n n
H1: IsLowerTriangular M
H2: IsLowerTriangular N
IsUpperTriangular (matrix_mult (matrix_transpose N) (matrix_transpose M))
  napply (upper_triangular_mult (R:=rng_op R)); assumption.
Defined.

(** The zero matrix is upper triangular. *)
Instance upper_triangular_zero {R : Ring@{i}} {n : nat}
  : IsUpperTriangular (matrix_zero R n n).
R: Ring
n: nat
IsUpperTriangular (matrix_zero R n n)
Proof.
R: Ring
n: nat
IsUpperTriangular (matrix_zero R n n)
  apply tr.
R: Ring
n: nat
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
(i < j)%nat -> entry (matrix_zero R n n) i j = 0
  by hnf; intros; rewrite entry_Build_Matrix.
Defined.

(** The zero matrix is lower triangular. *)
Instance lower_triangular_zero {R : Ring@{i}} {n : nat}
  : IsLowerTriangular (matrix_zero R n n).
R: Ring
n: nat
IsLowerTriangular (matrix_zero R n n)
Proof.
R: Ring
n: nat
IsLowerTriangular (matrix_zero R n n)
  unfold IsLowerTriangular.
R: Ring
n: nat
IsUpperTriangular (matrix_transpose (matrix_zero R n n))
  rewrite matrix_transpose_zero.
R: Ring
n: nat
IsUpperTriangular (matrix_zero R n n)
  exact _.
Defined.

(** The identity matrix is upper triangular. *)
Instance upper_triangular_identity@{i} {R : Ring@{i}} {n : nat}
  : IsUpperTriangular (identity_matrix R n).
R: Ring
n: nat
IsUpperTriangular (identity_matrix R n)
Proof.
R: Ring
n: nat
IsUpperTriangular (identity_matrix R n)
  unfold IsUpperTriangular.
R: Ring
n: nat
merely
  (forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
   (i < j)%nat -> entry (identity_matrix R n) i j = 0)
  apply tr@{i}.
R: Ring
n: nat
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
(i < j)%nat -> entry (identity_matrix R n) i j = 0
  intros i j Hi Hj lt_i_j.
R: Ring
n, i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
entry (identity_matrix R n) i j = 0
  rewrite entry_Build_Matrix@{i}.
R: Ring
n, i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
kronecker_delta i j = 0
  by apply kronecker_delta_lt.
Defined.

(** The identity matrix is lower triangular. *)
Instance lower_triangular_identity@{i} {R : Ring@{i}} {n : nat}
  : IsLowerTriangular (identity_matrix R n).
R: Ring
n: nat
IsLowerTriangular (identity_matrix R n)
Proof.
R: Ring
n: nat
IsLowerTriangular (identity_matrix R n)
  unfold IsLowerTriangular.
R: Ring
n: nat
IsUpperTriangular (matrix_transpose (identity_matrix R n))
  rewrite matrix_transpose_identity.
R: Ring
n: nat
IsUpperTriangular (identity_matrix R n)
  exact _.
Defined.

(** A diagonal matrix is upper triangular. *)
Instance upper_triangular_diag {R : Ring@{i}} {n : nat} (v : Vector R n)
  : IsUpperTriangular (matrix_diag v).
R: Ring
n: nat
v: Vector R n
IsUpperTriangular (matrix_diag v)
Proof.
R: Ring
n: nat
v: Vector R n
IsUpperTriangular (matrix_diag v)
  unfold IsUpperTriangular.
R: Ring
n: nat
v: Vector R n
merely
  (forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
   (i < j)%nat -> entry (matrix_diag v) i j = 0)
  apply tr.
R: Ring
n: nat
v: Vector R n
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
(i < j)%nat -> entry (matrix_diag v) i j = 0
  intros i j Hi Hj lt_i_j.
R: Ring
n: nat
v: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
entry (matrix_diag v) i j = 0
  rewrite entry_Build_Matrix.
R: Ring
n: nat
v: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
kronecker_delta i j * Vector.entry v i = 0
  rewrite kronecker_delta_lt.
R: Ring
n: nat
v: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
0 * Vector.entry v i = 0
R: Ring
n: nat
v: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
(i < j)%nat
  1: by rewrite rng_mult_zero_l.
R: Ring
n: nat
v: Vector R n
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
lt_i_j: (i < j)%nat
(i < j)%nat
  exact _.
Defined.

(** A diagonal matrix is lower triangular. *)
Instance lower_triangular_diag {R : Ring@{i}} {n : nat} (v : Vector R n)
  : IsLowerTriangular (matrix_diag v).
R: Ring
n: nat
v: Vector R n
IsLowerTriangular (matrix_diag v)
Proof.
R: Ring
n: nat
v: Vector R n
IsLowerTriangular (matrix_diag v)
  unfold IsLowerTriangular.
R: Ring
n: nat
v: Vector R n
IsUpperTriangular (matrix_transpose (matrix_diag v))
  rewrite matrix_transpose_diag.
R: Ring
n: nat
v: Vector R n
IsUpperTriangular (matrix_diag v)
  apply upper_triangular_diag.
Defined.

(** Upper triangular matrices are a subring of the ring of matrices. *)
Definition upper_triangular_matrix_ring@{i} (R : Ring@{i}) (n : nat)
  : Subring@{i i} (matrix_ring@{i} R n).
R: Ring
n: nat
Subring (matrix_ring R n)
Proof.
R: Ring
n: nat
Subring (matrix_ring R n)
  napply (Build_Subring' (fun M : matrix_ring R n => IsUpperTriangular M)).
R: Ring
n: nat
forall x : matrix_ring R n, IsHProp (IsUpperTriangular x)
R: Ring
n: nat
forall x y : matrix_ring R n,
IsUpperTriangular x -> IsUpperTriangular y -> IsUpperTriangular (x - y)
R: Ring
n: nat
forall x y : matrix_ring R n,
IsUpperTriangular x -> IsUpperTriangular y -> IsUpperTriangular (x * y)
R: Ring
n: nat
IsUpperTriangular 1
  -
R: Ring
n: nat
forall x : matrix_ring R n, IsHProp (IsUpperTriangular x) exact _.
  (* These can all be found by typeclass search, but being explicit makes this faster. *)
  -
R: Ring
n: nat
forall x y : matrix_ring R n,
IsUpperTriangular x -> IsUpperTriangular y -> IsUpperTriangular (x - y) intros x y ? ?; exact (upper_triangular_plus x (-y)).
  -
R: Ring
n: nat
forall x y : matrix_ring R n,
IsUpperTriangular x -> IsUpperTriangular y -> IsUpperTriangular (x * y) exact upper_triangular_mult.
  -
R: Ring
n: nat
IsUpperTriangular 1 exact upper_triangular_identity.
Defined.

(** Lower triangular matrices are a subring of the ring of matrices. *)
Definition lower_triangular_matrix_ring@{i} (R : Ring@{i}) (n : nat)
  : Subring@{i i} (matrix_ring R n).
R: Ring
n: nat
Subring (matrix_ring R n)
Proof.
R: Ring
n: nat
Subring (matrix_ring R n)
  napply (Build_Subring'@{i i} (fun M : matrix_ring R n => IsLowerTriangular M)).
R: Ring
n: nat
forall x : matrix_ring R n, IsHProp (IsLowerTriangular x)
R: Ring
n: nat
forall x y : matrix_ring R n,
IsLowerTriangular x -> IsLowerTriangular y -> IsLowerTriangular (x - y)
R: Ring
n: nat
forall x y : matrix_ring R n,
IsLowerTriangular x -> IsLowerTriangular y -> IsLowerTriangular (x * y)
R: Ring
n: nat
IsLowerTriangular 1
  -
R: Ring
n: nat
forall x : matrix_ring R n, IsHProp (IsLowerTriangular x) exact _.
  (* These can all be found by typeclass search, but being explicit makes this faster. *)
  -
R: Ring
n: nat
forall x y : matrix_ring R n,
IsLowerTriangular x -> IsLowerTriangular y -> IsLowerTriangular (x - y) intros x y ? ?; exact (lower_triangular_plus x (-y)).
  -
R: Ring
n: nat
forall x y : matrix_ring R n,
IsLowerTriangular x -> IsLowerTriangular y -> IsLowerTriangular (x * y) exact lower_triangular_mult.
  -
R: Ring
n: nat
IsLowerTriangular 1 exact lower_triangular_identity.
Defined.

(** ** Symmetric Matrices *)

(** A matrix is symmetric when it is equal to its transpose. *)
Class IsSymmetric {R : Ring@{i}} {n : nat} (M : Matrix@{i} R n n) : Type@{i}
  := matrix_transpose_issymmetric : matrix_transpose M = M.

Arguments matrix_transpose_issymmetric {R n} M {_}.

(** The zero matrix is symmetric. *)
Instance issymmetric_matrix_zero {R : Ring@{i}} {n : nat}
  : IsSymmetric (matrix_zero R n n)
  := matrix_transpose_zero.

(** The identity matrix is symmetric. *)
Instance issymmetric_matrix_identity {R : Ring@{i}} {n : nat}
  : IsSymmetric (identity_matrix R n)
  := matrix_transpose_identity.

(** The sum of two symmetric matrices is symmetric. *)
Instance issymmetric_matrix_plus {R : Ring@{i}} {n : nat}
  (M N : Matrix R n n) `{!IsSymmetric M} `{!IsSymmetric N}
  : IsSymmetric (matrix_plus M N).
R: Ring
n: nat
M, N: Matrix R n n
IsSymmetric0: IsSymmetric M
IsSymmetric1: IsSymmetric N
IsSymmetric (matrix_plus M N)
Proof.
R: Ring
n: nat
M, N: Matrix R n n
IsSymmetric0: IsSymmetric M
IsSymmetric1: IsSymmetric N
IsSymmetric (matrix_plus M N)
  unfold IsSymmetric.
R: Ring
n: nat
M, N: Matrix R n n
IsSymmetric0: IsSymmetric M
IsSymmetric1: IsSymmetric N
matrix_transpose (matrix_plus M N) = matrix_plus M N
  rewrite matrix_transpose_plus.
R: Ring
n: nat
M, N: Matrix R n n
IsSymmetric0: IsSymmetric M
IsSymmetric1: IsSymmetric N
matrix_plus (matrix_transpose M) (matrix_transpose N) = matrix_plus M N
  f_ap.
Defined.

(** The negation of a symmetric matrix is symmetric. *)
Instance issymmetric_matrix_negate {R : Ring@{i}} {n : nat}
  (M : Matrix R n n) `{!IsSymmetric M}
  : IsSymmetric (matrix_negate M).
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
IsSymmetric (matrix_negate M)
Proof.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
IsSymmetric (matrix_negate M)
  unfold IsSymmetric.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
matrix_transpose (matrix_negate M) = matrix_negate M
  rewrite matrix_transpose_negate.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
matrix_negate (matrix_transpose M) = matrix_negate M
  f_ap.
Defined.

(** A scalar multiple of a symmetric matrix is symmetric. *)
Instance issymmetric_matrix_scale {R : Ring@{i}} {n : nat}
  (r : R) (M : Matrix R n n) `{!IsSymmetric M}
  : IsSymmetric (matrix_lact r M).
R: Ring
n: nat
r: R
M: Matrix R n n
IsSymmetric0: IsSymmetric M
IsSymmetric (matrix_lact r M)
Proof.
R: Ring
n: nat
r: R
M: Matrix R n n
IsSymmetric0: IsSymmetric M
IsSymmetric (matrix_lact r M)
  unfold IsSymmetric.
R: Ring
n: nat
r: R
M: Matrix R n n
IsSymmetric0: IsSymmetric M
matrix_transpose (matrix_lact r M) = matrix_lact r M
  rewrite matrix_transpose_lact.
R: Ring
n: nat
r: R
M: Matrix R n n
IsSymmetric0: IsSymmetric M
matrix_lact r (matrix_transpose M) = matrix_lact r M
  f_ap.
Defined.

(** The transpose of a symmetric matrix is symmetric. *)
Instance issymmetric_matrix_transpose {R : Ring@{i}} {n : nat}
  (M : Matrix R n n) `{!IsSymmetric M}
  : IsSymmetric (matrix_transpose M).
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
IsSymmetric (matrix_transpose M)
Proof.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
IsSymmetric (matrix_transpose M)
  unfold IsSymmetric.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
matrix_transpose (matrix_transpose M) = matrix_transpose M
  rewrite matrix_transpose_transpose.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
M = matrix_transpose M
  by symmetry.
Defined.

(** A symmetric upper triangular matrix is diagonal. *)
Instance isdiagonal_upper_triangular_issymmetric {R : Ring@{i}} {n : nat}
  (M : Matrix R n n) `{!IsSymmetric M} {H : IsUpperTriangular M}
  : IsDiagonal M.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
H: IsUpperTriangular M
IsDiagonal M
Proof.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
H: IsUpperTriangular M
IsDiagonal M
  exists (matrix_diag_vector M).
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
H: IsUpperTriangular M
M = matrix_diag (matrix_diag_vector M)
  snapply path_matrix.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
H: IsUpperTriangular M
forall (i j : nat) (Hi : (i < n)%nat) (Hj : (j < n)%nat),
entry M i j = entry (matrix_diag (matrix_diag_vector M)) i j
  intros i j Hi Hj.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
H: IsUpperTriangular M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
entry M i j = entry (matrix_diag (matrix_diag_vector M)) i j
  rewrite entry_Build_Matrix, entry_Build_Vector.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
H: IsUpperTriangular M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
entry M i j = kronecker_delta i j * entry M i i
  strip_truncations.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
entry M i j = kronecker_delta i j * entry M i i
  destruct (dec (i = j)) as [p|np].
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
p: i = j
entry M i j = kronecker_delta i j * entry M i i
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
np: i <> j
entry M i j = kronecker_delta i j * entry M i i
  {
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
p: i = j
entry M i j = kronecker_delta i j * entry M i i destruct p.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i: nat
Hi, Hj: (i < n)%nat
H: forall (i0 j : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j < n)%nat),
(i0 < j)%nat -> entry M i0 j = 0
entry M i i = kronecker_delta i i * entry M i i
    rewrite kronecker_delta_refl.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i: nat
Hi, Hj: (i < n)%nat
H: forall (i0 j : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j < n)%nat),
(i0 < j)%nat -> entry M i0 j = 0
entry M i i = 1 * entry M i i
    rewrite rng_mult_one_l.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i: nat
Hi, Hj: (i < n)%nat
H: forall (i0 j : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j < n)%nat),
(i0 < j)%nat -> entry M i0 j = 0
entry M i i = entry M i i
    f_ap; apply path_ishprop. }
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
np: i <> j
entry M i j = kronecker_delta i j * entry M i i
  apply neq_iff_lt_or_gt in np.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
np: (i < j)%nat + (i > j)%nat
entry M i j = kronecker_delta i j * entry M i i
  destruct np as [l | l].
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
l: (i < j)%nat
entry M i j = kronecker_delta i j * entry M i i
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
l: (i > j)%nat
entry M i j = kronecker_delta i j * entry M i i
  -
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
l: (i < j)%nat
entry M i j = kronecker_delta i j * entry M i i rewrite (kronecker_delta_lt l).
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
l: (i < j)%nat
entry M i j = 0 * entry M i i
    rewrite rng_mult_zero_l.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
l: (i < j)%nat
entry M i j = 0
    by rewrite H.
  -
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
l: (i > j)%nat
entry M i j = kronecker_delta i j * entry M i i rewrite (kronecker_delta_gt l).
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
l: (i > j)%nat
entry M i j = 0 * entry M i i
    rewrite rng_mult_zero_l.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
l: (i > j)%nat
entry M i j = 0
    rewrite <- (matrix_transpose_issymmetric M).
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
l: (i > j)%nat
entry (matrix_transpose M) i j = 0
    rewrite entry_Build_Matrix.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
i, j: nat
Hi: (i < n)%nat
Hj: (j < n)%nat
H: forall (i0 j0 : nat) (Hi0 : (i0 < n)%nat) (Hj0 : (j0 < n)%nat),
(i0 < j0)%nat -> entry M i0 j0 = 0
l: (i > j)%nat
entry M j i = 0
    by rewrite H.
Defined.

(** A symmetric lower triangular matrix is diagonal. *)
Instance isdiagonal_lower_triangular_issymmetric {R : Ring@{i}} {n : nat}
  (M : Matrix R n n) `{!IsSymmetric M} `{!IsLowerTriangular M}
  : IsDiagonal M.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
IsLowerTriangular0: IsLowerTriangular M
IsDiagonal M
Proof.
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
IsLowerTriangular0: IsLowerTriangular M
IsDiagonal M
  rewrite <- (matrix_transpose_issymmetric M).
R: Ring
n: nat
M: Matrix R n n
IsSymmetric0: IsSymmetric M
IsLowerTriangular0: IsLowerTriangular M
IsDiagonal (matrix_transpose M)
  rapply isdiagonal_upper_triangular_issymmetric.
Defined.

(** Note that symmetric matrices do not form a subring (or subalgebra) but they do form a submodule of the module of matrices. *)

(** ** Skew-symmetric Matrices *)

(** A matrix is skew-symmetric when it is equal to the negation of its transpose. *)
Class IsSkewSymmetric {R : Ring@{i}} {n : nat} (M : Matrix@{i} R n n) : Type@{i}
  := matrix_transpose_isskewsymmetric : matrix_transpose M = matrix_negate M.

Arguments matrix_transpose_isskewsymmetric {R n} M {_}.

(** The zero matrix is skew-symmetric. *)
Instance isskewsymmetric_matrix_zero {R : Ring@{i}} {n : nat}
  : IsSkewSymmetric (matrix_zero R n n).
R: Ring
n: nat
IsSkewSymmetric (matrix_zero R n n)
Proof.
R: Ring
n: nat
IsSkewSymmetric (matrix_zero R n n)
  unfold IsSkewSymmetric.
R: Ring
n: nat
matrix_transpose (matrix_zero R n n) = matrix_negate (matrix_zero R n n)
  rewrite matrix_transpose_zero.
R: Ring
n: nat
matrix_zero R n n = matrix_negate (matrix_zero R n n)
  symmetry.
R: Ring
n: nat
matrix_negate (matrix_zero R n n) = matrix_zero R n n
  napply (rng_negate_zero (A:=matrix_ring R n)).
Defined.

(** The negation of a skew-symmetric matrix is skew-symmetric. *)
Instance isskewsymmetric_matrix_negate {R : Ring@{i}} {n : nat}
  (M : Matrix R n n) `{!IsSkewSymmetric M}
  : IsSkewSymmetric (matrix_negate M).
R: Ring
n: nat
M: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
IsSkewSymmetric (matrix_negate M)
Proof.
R: Ring
n: nat
M: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
IsSkewSymmetric (matrix_negate M)
  unfold IsSkewSymmetric.
R: Ring
n: nat
M: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
matrix_transpose (matrix_negate M) = matrix_negate (matrix_negate M)
  rewrite matrix_transpose_negate.
R: Ring
n: nat
M: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
matrix_negate (matrix_transpose M) = matrix_negate (matrix_negate M)
  f_ap.
Defined.

(** A scalar multiple of a skew-symmetric matrix is skew-symmetric. *)
Instance isskewsymmetric_matrix_scale {R : Ring@{i}} {n : nat}
  (r : R) (M : Matrix R n n) `{!IsSkewSymmetric M}
  : IsSkewSymmetric (matrix_lact r M).
R: Ring
n: nat
r: R
M: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
IsSkewSymmetric (matrix_lact r M)
Proof.
R: Ring
n: nat
r: R
M: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
IsSkewSymmetric (matrix_lact r M)
  unfold IsSkewSymmetric.
R: Ring
n: nat
r: R
M: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
matrix_transpose (matrix_lact r M) = matrix_negate (matrix_lact r M)
  rewrite matrix_transpose_lact.
R: Ring
n: nat
r: R
M: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
matrix_lact r (matrix_transpose M) = matrix_negate (matrix_lact r M)
  rhs_V napply (lm_neg (M:=Build_LeftModule _ (abgroup_matrix R n n) _) r M).
R: Ring
n: nat
r: R
M: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
matrix_lact r (matrix_transpose M) = lact r (- M)
  f_ap.
Defined.

(** The transpose of a skew-symmetric matrix is skew-symmetric. *)
Instance isskewsymmetric_matrix_transpose {R : Ring@{i}} {n : nat}
  (M : Matrix R n n) `{!IsSkewSymmetric M}
  : IsSkewSymmetric (matrix_transpose M).
R: Ring
n: nat
M: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
IsSkewSymmetric (matrix_transpose M)
Proof.
R: Ring
n: nat
M: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
IsSkewSymmetric (matrix_transpose M)
  unfold IsSkewSymmetric.
R: Ring
n: nat
M: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
matrix_transpose (matrix_transpose M) = matrix_negate (matrix_transpose M)
  rewrite <- matrix_transpose_negate.
R: Ring
n: nat
M: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
matrix_transpose (matrix_transpose M) = matrix_transpose (matrix_negate M)
  f_ap.
Defined.

(** The sum of two skew-symmetric matrices is skew-symmetric. *)
Instance isskewsymmetric_matrix_plus {R : Ring@{i}} {n : nat}
  (M N : Matrix R n n) `{!IsSkewSymmetric M} `{!IsSkewSymmetric N}
  : IsSkewSymmetric (matrix_plus M N).
R: Ring
n: nat
M, N: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
IsSkewSymmetric1: IsSkewSymmetric N
IsSkewSymmetric (matrix_plus M N)
Proof.
R: Ring
n: nat
M, N: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
IsSkewSymmetric1: IsSkewSymmetric N
IsSkewSymmetric (matrix_plus M N)
  unfold IsSkewSymmetric.
R: Ring
n: nat
M, N: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
IsSkewSymmetric1: IsSkewSymmetric N
matrix_transpose (matrix_plus M N) = matrix_negate (matrix_plus M N)
  rewrite matrix_transpose_plus.
R: Ring
n: nat
M, N: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
IsSkewSymmetric1: IsSkewSymmetric N
matrix_plus (matrix_transpose M) (matrix_transpose N) =
matrix_negate (matrix_plus M N)
  rhs napply (grp_inv_op (G:=abgroup_matrix R n n)).
R: Ring
n: nat
M, N: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
IsSkewSymmetric1: IsSkewSymmetric N
matrix_plus (matrix_transpose M) (matrix_transpose N) = sg_op (inv N) (inv M)
  rhs_V rapply AbelianGroup.abgroup_commutative.
R: Ring
n: nat
M, N: Matrix R n n
IsSkewSymmetric0: IsSkewSymmetric M
IsSkewSymmetric1: IsSkewSymmetric N
matrix_plus (matrix_transpose M) (matrix_transpose N) = sg_op (inv M) (inv N)
  f_ap.
Defined.

(** Skew-symmetric matrices degenerate to symmetric matrices in rings with characteristic 2. In odd characteristic the module of matrices can be decomposed into the direct sum of symmetric and skew-symmetric matrices. *)

Section MatrixCat.

  (** The wild category [MatrixCat R] of [R]-valued matrices. This category has natural numbers as objects and m x n matrices as the arrows between [m] and [n]. *)
  Definition MatrixCat (R : Ring) := nat.

  #[export] Instance isgraph_matrixcat {R : Ring} : IsGraph (MatrixCat R)
    := {| Hom := Matrix R |}.

  #[export] Instance is01cat_matrixcat {R : Ring} : Is01Cat (MatrixCat R).
R: Ring
Is01Cat (MatrixCat R)
  Proof.
R: Ring
Is01Cat (MatrixCat R)
    snapply Build_Is01Cat.
R: Ring
forall a : MatrixCat R, a $-> a
R: Ring
forall a b c : MatrixCat R, (b $-> c) -> (a $-> b) -> a $-> c
    -
R: Ring
forall a : MatrixCat R, a $-> a exact (identity_matrix R).
    -
R: Ring
forall a b c : MatrixCat R, (b $-> c) -> (a $-> b) -> a $-> c intros l m n M N.
R: Ring
l, m, n: MatrixCat R
M: m $-> n
N: l $-> m
l $-> n
      exact (matrix_mult N M).
  Defined.

  #[export] Instance is2graph_matrixcat {R : Ring} : Is2Graph (MatrixCat R)
    := is2graph_paths _.

  (** [MatrixCat R] forms a strong 1-category. *)
  #[export] Instance is1catstrong_matrixcat {R : Ring} : Is1Cat_Strong (MatrixCat R).
R: Ring
Is1Cat_Strong (MatrixCat R)
  Proof.
R: Ring
Is1Cat_Strong (MatrixCat R)
    snapply Build_Is1Cat_Strong.
R: Ring
forall a b : MatrixCat R, Is01Cat (a $-> b)
R: Ring
forall a b : MatrixCat R, Is0Gpd (a $-> b)
R: Ring
forall (a b c : MatrixCat R) (g : b $-> c), Is0Functor (cat_postcomp a g)
R: Ring
forall (a b c : MatrixCat R) (f : a $-> b), Is0Functor (cat_precomp c f)
R: Ring
forall (a b c d : MatrixCat R) (f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o g $o f = h $o (g $o f)
R: Ring
forall (a b c d : MatrixCat R) (f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o (g $o f) = h $o g $o f
R: Ring
forall (a b : MatrixCat R) (f : a $-> b), Id b $o f = f
R: Ring
forall (a b : MatrixCat R) (f : a $-> b), f $o Id a = f
    (* Most of the structure comes from typeclasses in WildCat.Paths. *)
    1-4: exact _.
R: Ring
forall (a b c d : MatrixCat R) (f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o g $o f = h $o (g $o f)
R: Ring
forall (a b c d : MatrixCat R) (f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o (g $o f) = h $o g $o f
R: Ring
forall (a b : MatrixCat R) (f : a $-> b), Id b $o f = f
R: Ring
forall (a b : MatrixCat R) (f : a $-> b), f $o Id a = f
    -
R: Ring
forall (a b c d : MatrixCat R) (f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o g $o f = h $o (g $o f) apply (associative_matrix_mult R).
    -
R: Ring
forall (a b c d : MatrixCat R) (f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o (g $o f) = h $o g $o f intros k l m n M N P.
R: Ring
k, l, m, n: MatrixCat R
M: k $-> l
N: l $-> m
P: m $-> n
P $o (N $o M) = P $o N $o M apply inverse.
R: Ring
k, l, m, n: MatrixCat R
M: k $-> l
N: l $-> m
P: m $-> n
P $o N $o M = P $o (N $o M) apply (associative_matrix_mult R).
    -
R: Ring
forall (a b : MatrixCat R) (f : a $-> b), Id b $o f = f apply right_identity_matrix_mult.
    -
R: Ring
forall (a b : MatrixCat R) (f : a $-> b), f $o Id a = f apply left_identity_matrix_mult.
  Defined.

(** TODO: Define [HasEquivs] for [MatrixCat].  *)

End MatrixCat.