diff --git a/Cubical/Algebra/Determinat/adjugate.agda b/Cubical/Algebra/Determinat/adjugate.agda
index a2f31ab3d..688359279 100644
--- a/Cubical/Algebra/Determinat/adjugate.agda
+++ b/Cubical/Algebra/Determinat/adjugate.agda
@@ -39,17 +39,11 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
   open Determinat ℓ P'
   open Coefficient (P')
 
+  -- Scalar multiplication
   _∘_ : {n m : ℕ} → R → FinMatrix R n m → FinMatrix R n m
   (a ∘ M) i j = a · (M i j)
 
-  deltaProp : {n : ℕ} → (k l : Fin n) → toℕ k <' toℕ l → δ k l ≡ 0r
-  deltaProp {suc n} zero (suc l) (s≤s le) = refl
-  deltaProp {suc n} (suc k) (suc l) (s≤s le) =  deltaProp {n} k l le
-
-  deltaPropSym : {n : ℕ} → (k l : Fin n) → toℕ l <' toℕ k → δ k l ≡ 0r
-  deltaPropSym {suc n} (suc k) (zero) (s≤s le) = refl
-  deltaPropSym {suc n} (suc k) (suc l) (s≤s le) =  deltaPropSym {n} k l le
-
+  -- Properties of ==
   ==Refl : {n : ℕ} → (k : Fin n) → k == k ≡ true
   ==Refl {n} zero = refl
   ==Refl {suc n} (suc k) = ==Refl {n} k
@@ -60,6 +54,15 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
   ==Sym {suc n} (suc k) zero = refl
   ==Sym {suc n} (suc k) (suc l) = ==Sym {n} k l
 
+  -- Properties of the Kronecker Delta
+  deltaProp : {n : ℕ} → (k l : Fin n) → toℕ k <' toℕ l → δ k l ≡ 0r
+  deltaProp {suc n} zero (suc l) (s≤s le) = refl
+  deltaProp {suc n} (suc k) (suc l) (s≤s le) =  deltaProp {n} k l le
+
+  deltaPropSym : {n : ℕ} → (k l : Fin n) → toℕ l <' toℕ k → δ k l ≡ 0r
+  deltaPropSym {suc n} (suc k) (zero) (s≤s le) = refl
+  deltaPropSym {suc n} (suc k) (suc l) (s≤s le) =  deltaPropSym {n} k l le
+
   deltaPropEq : {n : ℕ} → (k l : Fin n) → k ≡ l → δ k l ≡ 1r
   deltaPropEq k l e =
     δ k l
@@ -71,12 +74,12 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
 
   deltaComm : {n : ℕ} → (k l : Fin n) → δ k l ≡ δ l k
   deltaComm k l = cong (λ a → if a then 1r else 0r) (==Sym k l)
-  
 
   -- Definition of the cofactor matrix 
   cof : {n : ℕ} → FinMatrix R n n → FinMatrix R n n
   cof {suc n} M i j = (MF (toℕ i +ℕ toℕ j)) ·  det {n} (minor i j M)
 
+  -- Behavior of the cofactor matrix under transposition
   cofTransp : {n : ℕ} → (M : FinMatrix R n n) → (i j : Fin n) → cof (M ᵗ) i j ≡ cof M j i
   cofTransp {suc n} M i j =
     MF (toℕ i +ℕ toℕ j) ·  det (minor i j (M ᵗ))
@@ -92,10 +95,11 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
   adjugate : {n : ℕ} → FinMatrix R n n → FinMatrix R n n
   adjugate M i j = cof M j i
 
+  -- Behavior of the adjugate matrix under transposition
   adjugateTransp : {n : ℕ} → (M : FinMatrix R n n) → (i j : Fin n) → adjugate (M ᵗ) i j ≡ adjugate M j i
   adjugateTransp M i j = cofTransp M j i
 
-
+  -- Properties of WeakenFin
   weakenPredFinLt : {n : ℕ} → (k l : Fin (suc (suc n))) → toℕ k <' toℕ l → k ≤'Fin weakenFin (predFin l)
   weakenPredFinLt {zero} zero one (s≤s z≤) = z≤
   weakenPredFinLt {zero} one one (s≤s ())
@@ -109,6 +113,7 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
   sucPredFin {zero} (suc k) (suc l) le = refl
   sucPredFin {suc n} zero (suc l) le = refl
   sucPredFin {suc n} (suc k) (suc l) (s≤s le) = refl
+
   
   adjugatePropAux1a :  {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → (k l : Fin (suc (suc n))) → toℕ k <' toℕ l →
    ∑
@@ -612,7 +617,7 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
            (MF (toℕ (predFin l) +ℕ toℕ z₁) · minor k z M (predFin l) z₁ ·
             det (minor (predFin l) z₁ (minor k z M)))))
       (λ i j →
-        DetRowAux2
+        distributeOne
         (ind> (toℕ i) (toℕ j))
         (M l i · MF (toℕ k +ℕ toℕ i) ·
           (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j ·
@@ -1506,7 +1511,7 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
             minor k i M (strongenFin l le) j
             · det (minor (strongenFin l le) j (minor k i M)))))
       (λ i j →
-        DetRowAux2
+        distributeOne
         (ind> (toℕ i) (toℕ j))
         ( M l i · MF (toℕ k +ℕ toℕ i) ·
             (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
@@ -1828,8 +1833,6 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
     0r
     ∎
 
-
-
   adjugateInvRLcomponent : {n : ℕ} → (M : FinMatrix R n n) → (k l : Fin n) → toℕ k <' toℕ l → (M ⋆ adjugate M) k l ≡  (det M ∘ 𝟙) k l
   adjugateInvRLcomponent {suc n} M k l le = 
     ∑ (λ i → M k i · (MF(toℕ l +ℕ toℕ i) · det(minor l i M)) )
@@ -1840,7 +1843,7 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
     ≡⟨ cong (λ a → det M · a) (sym (deltaProp k l le)) ⟩
     (det M ∘ 𝟙) k l
     ∎
-  
+
   FinCompare : {n : ℕ} → (k l : Fin n) →  (k ≡ l) ⊎ ((toℕ k <' toℕ l) ⊎ (toℕ l <' toℕ k))
   FinCompare {zero} () ()
   FinCompare {suc n} zero zero = inl refl
@@ -1851,7 +1854,8 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
   ... | inr (inl x) = inr (inl (s≤s x))
   ... | inr (inr x) = inr (inr (s≤s x))
   
-
+  -- The adjugate matrix divided by the determinant is the right inverse.
+  -- Component-wise version
   adjugateInvRComp : {n : ℕ} → (M : FinMatrix R n n) → (k l : Fin n)  → (M ⋆ adjugate M) k l ≡  (det M ∘ 𝟙) k l
   adjugateInvRComp {zero} M () ()
   adjugateInvRComp {suc n} M k l  with FinCompare k l
@@ -1890,6 +1894,8 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
   ... | inr (inl x) = adjugateInvRLcomponent M k l x
   ... | inr (inr x) =  adjugateInvRGcomponent M k l x
 
+  -- The adjugate matrix divided by the determinant is the left inverse.
+  -- Component-wise version
   adjugateInvLComp : {n : ℕ} → (M : FinMatrix R n n) → (k l : Fin n)  → (adjugate M ⋆ M) k l ≡  (det M ∘ 𝟙) k l
   adjugateInvLComp M k l =
     (adjugate M ⋆ M) k l
@@ -1917,9 +1923,10 @@ module adjugate (ℓ : Level) (P' : CommRing ℓ) where
     (det M · 𝟙 k l)
     ∎
   
-
+  -- The adjugate matrix divided by the determinant is the right inverse.
   adjugateInvR : {n : ℕ} → (M : FinMatrix R n n)  → M ⋆ adjugate M ≡  det M ∘ 𝟙
   adjugateInvR M = funExt₂ (λ k l →  adjugateInvRComp M k l)
 
+  -- The adjugate matrix divided by the determinant is the left inverse.
   adjugateInvL : {n : ℕ} → (M : FinMatrix R n n)  → adjugate M ⋆ M ≡  det M ∘ 𝟙
   adjugateInvL M = funExt₂ (λ k l →  adjugateInvLComp M k l)
diff --git a/Cubical/Algebra/Determinat/det.agda b/Cubical/Algebra/Determinat/det.agda
index 0ead56c92..3f61eec80 100644
--- a/Cubical/Algebra/Determinat/det.agda
+++ b/Cubical/Algebra/Determinat/det.agda
@@ -42,7 +42,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
   MF zero = 1r
   MF (suc i) = (- 1r) · (MF i)
 
-  --Multiplicity of the minor factor
+  --Properties of the minor factor
   sumMF : (i j : ℕ) → MF (i +ℕ j) ≡ (MF i) · (MF j)
   sumMF zero j =
     MF j
@@ -63,6 +63,30 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
   sucMFRev : (i : ℕ) → MF i ≡ (- 1r) · MF (suc i)
   sucMFRev i = solve! P'
 
+  MFplusZero : {n : ℕ} → (i : Fin n) →   MF (toℕ i +ℕ zero) ≡ MF (toℕ i)
+  MFplusZero i =
+    MF (toℕ i +ℕ zero)
+    ≡⟨ sumMF (toℕ i) zero ⟩
+    (MF (toℕ i) · MF zero)
+    ≡⟨ ·IdR (MF (toℕ i)) ⟩
+    MF (toℕ i)
+    ∎
+
+  MFsucsuc :  {n m : ℕ} → (j : Fin n) → (k : Fin m) →
+    MF (toℕ (suc j) +ℕ (toℕ (suc k))) ≡ MF (toℕ j +ℕ toℕ k)
+  MFsucsuc j k =
+    MF (toℕ (suc j) +ℕ toℕ (suc k))
+    ≡⟨ sumMF (toℕ (suc j)) (toℕ (suc k)) ⟩
+    (MF (toℕ (suc j)) · MF (toℕ (suc k)))
+    ≡⟨ refl ⟩
+    ((- 1r) · MF (toℕ j) · ((- 1r) · MF (toℕ k)) )
+    ≡⟨ solve! P' ⟩
+    ( MF (toℕ j) · MF ( toℕ k))
+    ≡⟨ sym (sumMF (toℕ j) (toℕ k))⟩ 
+    MF (toℕ j +ℕ toℕ k)
+    ∎
+
+  -- Other small lemmata
   +Compat : {a b c d : R} → a ≡ b → c ≡ d → a + c ≡ b + d
   +Compat {a} {b} {c} {d} eq1 eq2 =
    a + c
@@ -71,6 +95,9 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
    ≡⟨ cong (λ x → b + x) eq2 ⟩
    b + d
    ∎
+
+  distributeOne : (a b : R) → b ≡ a · b + (1r + (- a)) · b
+  distributeOne a b = solve! P'
   
   -- Definition of the determinat by using Laplace expansion
   det : ∀ {n} → FinMatrix R n n → R
@@ -164,9 +191,6 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
       det (minor zero j (minor k i M)))
      ∎
 
-  DetRowAux2 : (a b : R) → b ≡ a · b + (1r + (- a)) · b
-  DetRowAux2 a b = solve! P'
-
   DetRowAux3a :
     {n : ℕ} → (k : Fin (suc n)) →
     (M : FinMatrix R (suc (suc n)) (suc (suc n))) → 
@@ -952,7 +976,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
              minor (suc k) i M zero j
              · det (minor zero j (minor (suc k) i M))))
         (λ i j →
-          DetRowAux2 (ind> (toℕ i) (toℕ j))
+          distributeOne (ind> (toℕ i) (toℕ j))
           (MF (toℕ (suc k) +ℕ toℕ i +ℕ toℕ j) · M (suc k) i ·
           minor (suc k) i M zero j · det (minor zero j (minor (suc k) i M))))
     ⟩
@@ -1152,7 +1176,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
          · det (minor k z₁ (minor zero z M)))
      (λ i j →
        sym
-       (DetRowAux2
+       (distributeOne
        (ind> (toℕ i) (toℕ j))
        (MF (toℕ (suc k) +ℕ toℕ (suc j) +ℕ toℕ i) · minor zero i M k j ·
          M zero i · det (minor k j (minor zero i M)))))
@@ -1338,7 +1362,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
           det (minor i zero (minor zero (suc j) M))))
        ∎)
    
-  
+  -- The determinant can also be expanded along the first column.
   DetRowColumn : ∀ {n} →  (M : FinMatrix R (suc n) (suc n)) →
      detC zero M ≡ det M
   DetRowColumn {zero} M = refl
@@ -1960,20 +1984,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
         i
         j)
 
-  MFsucsuc :  {n m : ℕ} → (j : Fin n) → (k : Fin m) →
-    MF (toℕ (suc j) +ℕ (toℕ (suc k))) ≡ MF (toℕ j +ℕ toℕ k)
-  MFsucsuc j k =
-    MF (toℕ (suc j) +ℕ toℕ (suc k))
-    ≡⟨ sumMF (toℕ (suc j)) (toℕ (suc k)) ⟩
-    (MF (toℕ (suc j)) · MF (toℕ (suc k)))
-    ≡⟨ refl ⟩
-    ((- 1r) · MF (toℕ j) · ((- 1r) · MF (toℕ k)) )
-    ≡⟨ solve! P' ⟩
-    ( MF (toℕ j) · MF ( toℕ k))
-    ≡⟨ sym (sumMF (toℕ j) (toℕ k))⟩ 
-    MF (toℕ j +ℕ toℕ k)
-    ∎
-
+  -- The determinant expanded along a column is independent of the chosen column.
   DetColumnZero : ∀ {n} → (k : Fin (suc n)) → (M : FinMatrix R (suc n) (suc n)) →
     detC k M ≡ detC zero M
   DetColumnZero {zero} zero M = refl
@@ -2046,7 +2057,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
            (MF (toℕ z₁ +ℕ zero) · minor z (suc k) M z₁ zero ·
             det (minor z₁ zero (minor z (suc k) M)))))
       (λ i j →
-        DetRowAux2
+        distributeOne
           (ind> (toℕ i) (toℕ j))
           (MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) ·
           (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero ·
@@ -2285,7 +2296,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
              (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k ·
               det (minor j k (minor i zero M)))))
        (λ i j → sym
-                (DetRowAux2 ( ind> (toℕ i) (toℕ j) )
+                (distributeOne ( ind> (toℕ i) (toℕ j) )
                 ((MF (toℕ i +ℕ zero) · M i zero ·
                 (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k ·
                 det (minor j k (minor i zero M))))))) ⟩
@@ -2388,6 +2399,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
     detC zero M
     ∎
 
+  -- The determinant expanded along a column is the regular determinant.
   DetColumn : ∀ {n} → (k : Fin (suc n)) → (M : FinMatrix R (suc n) (suc n)) →
     detC k M ≡ det M
   DetColumn k M =
@@ -2405,6 +2417,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
   ∑Mul1r = Sum.∑Mul1r (CommRing→Ring P')
   ∑Mulr1 = Sum.∑Mulr1 (CommRing→Ring P')
 
+  -- The determinant of the zero matrix is 0.
   detZero : {n : ℕ} → det {suc n} 𝟘 ≡ 0r
   detZero {n} =
     ∑Zero
@@ -2421,6 +2434,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
         ∎
         )
 
+  --The determinant of the identity matrix is 1.
   detOne : {n : ℕ} → det {n} 𝟙 ≡ 1r
   detOne {zero} = refl
   detOne {suc n} =
@@ -2454,15 +2468,7 @@ module Determinat (ℓ : Level) (P' : CommRing ℓ) where
     1r
     ∎
 
-  MFplusZero : {n : ℕ} → (i : Fin n) →   MF (toℕ i +ℕ zero) ≡ MF (toℕ i)
-  MFplusZero i =
-    MF (toℕ i +ℕ zero)
-    ≡⟨ sumMF (toℕ i) zero ⟩
-    (MF (toℕ i) · MF zero)
-    ≡⟨ ·IdR (MF (toℕ i)) ⟩
-    MF (toℕ i)
-    ∎
-  
+  --The determinant remains unchanged under transposition.
   detTransp : {n : ℕ} → (M : FinMatrix R n n) → det M ≡ det (M ᵗ)
   detTransp {zero} M = refl
   detTransp {suc n} M =
diff --git a/Cubical/Algebra/Determinat/minor.agda b/Cubical/Algebra/Determinat/minor.agda
deleted file mode 100644
index 6ba1082d1..000000000
--- a/Cubical/Algebra/Determinat/minor.agda
+++ /dev/null
@@ -1,186 +0,0 @@
-{-# OPTIONS --cubical #-}
-
-module minor where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.Equiv
-open import Cubical.Algebra.Matrix
-open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_
-                                       ; +-comm to +ℕ-comm
-                                       ; +-assoc to +ℕ-assoc
-                                       ; ·-assoc to ·ℕ-assoc)
-open import Cubical.Data.Vec.Base using (_∷_; [])
-open import Cubical.Foundations.Structure using (⟨_⟩)
-open import Cubical.Data.FinData
-open import Cubical.Data.FinData.Order using (_<'Fin_; _≤'Fin_)
-open import Cubical.Algebra.Ring
-open import Cubical.Algebra.Ring.Base
-open import Cubical.Algebra.Ring.BigOps
-open import Cubical.Algebra.Monoid.BigOp
-open import Cubical.Algebra.CommRing
-open import Cubical.Algebra.CommRing.Base
-open import Cubical.Data.Nat.Order 
-open import Cubical.Tactics.CommRingSolver
-
-module Minor (ℓ : Level) where
-
-  -- definition and properties to remove one Index, i.e. (removeIndex i) is the monoton ebbeding from {0,...,n-1} to {0,...,n} ommiting i.
-
-  removeIndex : {n : ℕ} → Fin (suc n) → Fin n → Fin (suc n)
-  removeIndex zero k = suc k
-  removeIndex (suc i) zero = zero
-  removeIndex (suc i) (suc k) = suc (removeIndex i k)
-
-  -- On {0,...,i-1} the map (removeIndex i) is the identity.
-  removeIndexId : {n : ℕ} → (i : Fin (suc n)) → (k : Fin n) → (suc k) ≤'Fin i → (removeIndex i k) ≡ weakenFin k
-  removeIndexId (suc i) zero le = refl
-  removeIndexId (suc i) (suc k) (s≤s le) =  cong (λ a → suc a) (removeIndexId i k le)
-
-  -- On {i,...,n-1} the map (removeIndex i) is the successor function.
-  removeIndexSuc : {n : ℕ} → (i : Fin (suc n)) → (k : Fin n) → i ≤'Fin weakenFin k  → (removeIndex i k) ≡ suc k
-  removeIndexSuc zero k le = refl
-  removeIndexSuc (suc i) (suc k) (s≤s le) = cong (λ a → suc a) (removeIndexSuc i k le)
-
-  -- A formula for commuting removeIndex maps
-  removeIndexComm :  {n : ℕ} → (i j : Fin (suc n)) → (k : Fin n) → i ≤'Fin j →
-    removeIndex (suc j) (removeIndex i k) ≡ removeIndex (weakenFin i) (removeIndex j k) 
-  removeIndexComm zero j k le = refl
-  removeIndexComm (suc i) (suc j) zero le = refl
-  removeIndexComm (suc i) (suc j) (suc k) (s≤s le) =  cong (λ a → suc a) (removeIndexComm i j k le)
-
-  -- remove the j-th column of a matrix
-  
-  remove-column : {A : Type ℓ} {n m : ℕ} (j : Fin (suc m)) (M : FinMatrix A n (suc m)) → FinMatrix A n m
-  remove-column j M k l = M k (removeIndex j l)
-
-  remove-column-comm :  {A : Type ℓ} {n m : ℕ} (i : Fin (suc m)) (j : Fin (suc m)) (M : FinMatrix A n (suc (suc m))) (k : Fin n) (l : Fin  m) →
-    j ≤'Fin i →
-    remove-column j (remove-column (suc i) M) k l ≡  remove-column i (remove-column (weakenFin j) M) k l
-  remove-column-comm i j M k l le =
-    remove-column j (remove-column (suc i) M) k l
-    ≡⟨  refl ⟩
-     M k (removeIndex (suc i) (removeIndex j l))
-    ≡⟨ cong (λ a → M k a) ( removeIndexComm j i l le) ⟩
-    M k (removeIndex (weakenFin j) (removeIndex i l))
-    ≡⟨ refl ⟩
-     remove-column i (remove-column (weakenFin j) M) k l
-    ∎
-     
-  -- remove the i-th row of a matrix
-  remove-row : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n)) (M : FinMatrix A (suc n) m) → FinMatrix A n m
-  remove-row i M k l = M (removeIndex i k) l
-
-  remove-row-comm : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n)) (j : Fin (suc n)) (M : FinMatrix A (suc (suc n)) m) (k : Fin n) (l : Fin  m) →
-    j ≤'Fin i →
-    remove-row j (remove-row (suc i) M) k l ≡  remove-row i (remove-row (weakenFin j) M) k l
-  remove-row-comm i j M k l le =
-    remove-row j (remove-row (suc i) M) k l
-    ≡⟨ refl ⟩
-      M (removeIndex (suc i) (removeIndex j k)) l
-    ≡⟨ cong (λ a → M a l) ( removeIndexComm j i k le) ⟩
-    M (removeIndex (weakenFin j) (removeIndex i k)) l
-    ≡⟨ refl ⟩
-     remove-row i (remove-row (weakenFin j) M) k l
-    ∎
-  
-  remove-column-row-comm : {A : Type ℓ} {n m : ℕ}  (i : Fin (suc n)) (j : Fin (suc m)) (M : FinMatrix A (suc n) (suc m)) (k : Fin n) (l : Fin m) →  (remove-row i (remove-column j M)) k l ≡  (remove-column j (remove-row i M)) k l
-  remove-column-row-comm i j M k l = refl
-  
-  -- Calculating of the minor.
-  minor : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n)) (j : Fin (suc m)) (M : FinMatrix A (suc n) (suc m)) → FinMatrix A n m
-  minor i j M = remove-column j (remove-row i M)
-
-  -- Compatability of the minor with the equality.
-  minorComp : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n)) (j : Fin (suc m)) (M N : FinMatrix A (suc n) (suc m)) → ((i : Fin (suc n)) → (j : Fin (suc m)) → M i j ≡ N i j ) → (k : Fin n) → (l : Fin m) →  minor i j M k l ≡ minor i j N k l
-  minorComp {n = suc n} {suc m} i j M N f k l = f (removeIndex i k) (removeIndex j l)
-
-  -- Formulas to commute minors
-  minorComm0 : {A : Type ℓ} {n m : ℕ} (i₁ i₂ : Fin (suc n)) (j₁ j₂ : Fin (suc m)) (k : Fin n) (l : Fin m) (M : FinMatrix A (suc (suc n)) (suc (suc m))) →
-    i₂ ≤'Fin i₁ → j₂ ≤'Fin j₁ →  
-    minor i₂ j₂ (minor (suc i₁) (suc j₁) M) k l ≡ minor i₁ j₁ (minor (weakenFin i₂) (weakenFin j₂) M) k l
-  minorComm0 i₁ i₂ j₁ j₂ k l M lei lej =
-    M (removeIndex (suc i₁) (removeIndex i₂ k))
-      (removeIndex (suc j₁) (removeIndex j₂ l))
-    ≡⟨ cong (λ a →  M a (removeIndex (suc j₁) (removeIndex j₂ l))) (removeIndexComm i₂ i₁ k lei) ⟩
-    M (removeIndex (weakenFin i₂) (removeIndex i₁ k))
-      (removeIndex (suc j₁) (removeIndex j₂ l))
-    ≡⟨ cong (λ a →  M (removeIndex (weakenFin i₂) (removeIndex i₁ k)) a ) ((removeIndexComm j₂ j₁ l lej)) ⟩
-    M (removeIndex (weakenFin i₂) (removeIndex i₁ k))
-      (removeIndex (weakenFin j₂) (removeIndex j₁ l))
-    ∎
-
-  minorComm1 : {A : Type ℓ} {n m : ℕ} (i₁ i₂ : Fin (suc n)) (j₁ j₂ : Fin (suc m)) (k : Fin n) (l : Fin m) (M : FinMatrix A (suc (suc n)) (suc (suc m))) →
-   i₂ ≤'Fin i₁ → j₁ ≤'Fin j₂ →  
-   minor i₂ j₂ (minor (suc i₁) (weakenFin j₁) M) k l ≡ minor i₁ j₁ (minor (weakenFin i₂) (suc j₂) M) k l
-
-  minorComm1 i₁ i₂ j₁ j₂ k l M lei lej =
-    M (removeIndex (suc i₁) (removeIndex i₂ k))
-      (removeIndex (weakenFin j₁) (removeIndex j₂ l))
-    ≡⟨ cong (λ a → M a (removeIndex (weakenFin j₁) (removeIndex j₂ l))) ((removeIndexComm i₂ i₁ k lei)) ⟩
-    M (removeIndex (weakenFin i₂) (removeIndex i₁ k))
-      (removeIndex (weakenFin j₁) (removeIndex j₂ l))
-    ≡⟨ cong (λ a → M (removeIndex (weakenFin i₂) (removeIndex i₁ k)) a) (sym ((removeIndexComm j₁ j₂ l lej))) ⟩
-    M (removeIndex (weakenFin i₂) (removeIndex i₁ k))
-      (removeIndex (suc j₂) (removeIndex j₁ l))
-    ∎
-
-  minorComm2 : {A : Type ℓ} {n m : ℕ} (i₁ i₂ : Fin (suc n)) (j₁ j₂ : Fin (suc m)) (k : Fin n) (l : Fin m) (M : FinMatrix A (suc (suc n)) (suc (suc m))) →
-   i₁ ≤'Fin i₂ → j₂ ≤'Fin j₁ →  
-   minor i₂ j₂ (minor (weakenFin i₁) (suc j₁) M) k l ≡ minor i₁ j₁ (minor (suc i₂) (weakenFin j₂) M) k l
-
-  minorComm2 i₁ i₂ j₁ j₂ k l M lei lej =
-   M (removeIndex (weakenFin i₁) (removeIndex i₂ k))
-     (removeIndex (suc j₁) (removeIndex j₂ l))
-   ≡⟨ cong (λ a → M a  (removeIndex (suc j₁) (removeIndex j₂ l))) (sym ((removeIndexComm i₁ i₂ k lei))) ⟩
-   M (removeIndex (suc i₂) (removeIndex i₁ k))
-     (removeIndex (suc j₁) (removeIndex j₂ l))
-   ≡⟨ cong (λ a →  M (removeIndex (suc i₂) (removeIndex i₁ k)) a) ((removeIndexComm j₂ j₁ l lej)) ⟩
-   M (removeIndex (suc i₂) (removeIndex i₁ k))
-     (removeIndex (weakenFin j₂) (removeIndex j₁ l))
-   ∎
-
-  --Formulas to compute compute the entries of the minor.
-  minorIdId : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n))(j : Fin (suc m)) (k : Fin n)(l : Fin m) (M : FinMatrix A (suc n) (suc m)) →
-    suc k ≤'Fin i → suc l ≤'Fin j →
-    minor i j M k l ≡ M (weakenFin k) (weakenFin l)
-  minorIdId i j k l M lei lej =
-    M  (removeIndex i k) (removeIndex j l)
-    ≡⟨ cong (λ a → M a (removeIndex j l)) (removeIndexId i k lei) ⟩
-    M (weakenFin k) (removeIndex j l)
-    ≡⟨ cong (λ a → M (weakenFin k) a) (removeIndexId j l lej) ⟩
-    M (weakenFin k) (weakenFin l)
-    ∎
-
-  minorSucSuc : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n))(j : Fin (suc m)) (k : Fin n)(l : Fin m) (M : FinMatrix A (suc n) (suc m)) →
-    i ≤'Fin weakenFin k → j ≤'Fin weakenFin l →
-    minor i j M k l ≡ M (suc k) (suc l)
-  minorSucSuc i j k l M lei lej = 
-    M  (removeIndex i k) (removeIndex j l)
-    ≡⟨ cong (λ a → M a (removeIndex j l)) (removeIndexSuc i k lei) ⟩
-    M (suc k) (removeIndex j l)
-    ≡⟨ cong (λ a → M (suc k) a) (removeIndexSuc j l lej) ⟩
-    M (suc k) (suc l)
-    ∎
-
-  minorIdSuc : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n))(j : Fin (suc m)) (k : Fin n)(l : Fin m) (M : FinMatrix A (suc n) (suc m)) →
-    suc k ≤'Fin i → j ≤'Fin weakenFin l →
-    minor i j M k l ≡ M (weakenFin k) (suc l)
-  minorIdSuc i j k l M lei lej =
-    M  (removeIndex i k) (removeIndex j l)
-    ≡⟨ cong (λ a → M a (removeIndex j l)) (removeIndexId i k lei) ⟩
-    M (weakenFin k) (removeIndex j l)
-    ≡⟨ cong (λ a → M (weakenFin k) a) (removeIndexSuc j l lej) ⟩
-    M (weakenFin k) (suc l)
-    ∎
-
-  minorSucId : {A : Type ℓ} {n m : ℕ} (i : Fin (suc n))(j : Fin (suc m)) (k : Fin n)(l : Fin m) (M : FinMatrix A (suc n) (suc m)) →
-    i ≤'Fin weakenFin k → suc l ≤'Fin j →
-    minor i j M k l ≡ M (suc k) (weakenFin l)
-  minorSucId i j k l M lei lej = 
-    M  (removeIndex i k) (removeIndex j l)
-    ≡⟨ cong (λ a → M a (removeIndex j l)) (removeIndexSuc i k lei) ⟩
-    M (suc k) (removeIndex j l)
-    ≡⟨ cong (λ a → M (suc k) a) (removeIndexId j l lej) ⟩
-    M (suc k) (weakenFin l)
-    ∎
-