Draft: Use polynomials to finish off the remainder of the proof

.gitignore

@@ -35,3 +35,4 @@ nra.cache
 .DS_Store
 CoqMakefile
 CoqMakefile.conf
+tags

Helpers/DiagonalHelpers.v

@@ -1,4 +1,5 @@
 Require Import QuantumLib.Eigenvectors.
+Require Import QuantumLib.Matrix.
 Require Import MatrixHelpers.
 Require Import GateHelpers.
 

Helpers/MatrixHelpers.v

@@ -82,6 +82,12 @@ Proof.
   unfold diag2, Determinant, big_sum, parity, get_minor; lca.
 Qed.
 
+Lemma Det_diag4 : forall (c1 c2 c3 c4 : C), Determinant (diag4 c1 c2 c3 c4) = c1 * c2 * c3 * c4.
+Proof.
+  intros.
+  unfold diag4, Determinant, big_sum, parity, get_minor; lca.
+Qed.
+
 Lemma row_out_of_bounds: forall {m n} (A : Matrix m n) (i : nat),
   WF_Matrix A -> (i >= m)%nat -> forall (j : nat), A i j = C0.
 Proof.
@@ -593,6 +599,9 @@ Proof.
   apply Coq.Logic.Classical_Prop.or_to_imply.
 Qed.
 
+Definition Mscale_id {n} (x : C) : Square n :=
+  fun i j => if i =? j then x else 0.
+
 Lemma Mscale_access {m n}: forall (a : C) (B : Matrix m n) (i j : nat),
 a * (B i j) = (a .* B) i j.
 Proof.