diff --git a/Cubical/Algebra/Determinat/Adjugate.agda b/Cubical/Algebra/Determinat/Adjugate.agda
new file mode 100644
index 000000000..a61574e18
--- /dev/null
+++ b/Cubical/Algebra/Determinat/Adjugate.agda
@@ -0,0 +1,1933 @@
+{-# OPTIONS --cubical #-}
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.Determinat.Adjugate where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Algebra.Matrix
+open import Cubical.Algebra.Matrix.CommRingCoefficient
+open import Cubical.Functions.FunExtEquiv
+open import Cubical.Data.Bool
+open import Cubical.Data.Sum
+open import Cubical.Foundations.Structure using (⟨_⟩)
+open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_
+ ; +-comm to +ℕ-comm
+ ; +-assoc to +ℕ-assoc
+ ; ·-assoc to ·ℕ-assoc)
+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.Algebra.Semiring
+open import Cubical.Data.Int.Base using (pos; negsuc)
+open import Cubical.Data.Vec.Base using (_∷_; [])
+open import Cubical.Data.Nat.Order
+open import Cubical.Tactics.CommRingSolver
+
+open import Cubical.Algebra.Determinat.Minor
+open import Cubical.Algebra.Determinat.RingSum
+open import Cubical.Algebra.Determinat.Base
+
+module Adjugate (ℓ : Level) (P' : CommRing ℓ) where
+ open Cubical.Algebra.Determinat.Minor.Minor ℓ
+ open Cubical.Algebra.Determinat.RingSum.RingSum ℓ P'
+ open RingStr (snd (CommRing→Ring P'))
+ open Cubical.Algebra.Determinat.Base.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)
+
+ -- Properties of ==
+ ==Refl : {n : ℕ} → (k : Fin n) → k == k ≡ true
+ ==Refl {n} zero = refl
+ ==Refl {suc n} (suc k) = ==Refl {n} k
+
+ ==Sym : {n : ℕ} → (k l : Fin n) → k == l ≡ l == k
+ ==Sym {suc n} zero zero = refl
+ ==Sym {suc n} zero (suc l) = refl
+ ==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
+ ≡⟨ cong (λ a → δ a l) e ⟩
+ δ l l
+ ≡⟨ cong (λ a → if a then 1r else 0r) (==Refl l) ⟩
+ 1r
+ ∎
+
+ 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 ᵗ))
+ ≡⟨ cong (λ a → MF (toℕ i +ℕ toℕ j) · a) (detTransp ((minor j i M ᵗ))) ⟩
+ (MF (toℕ i +ℕ toℕ j) · det (minor j i M))
+ ≡⟨
+ cong
+ (λ a → MF (a) · det (minor j i M)) (+ℕ-comm (toℕ i) (toℕ j)) ⟩
+ (MF (toℕ j +ℕ toℕ i) · det (minor j i M))
+ ∎
+
+ -- Definition of the adjugate matrix
+ 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 ())
+ weakenPredFinLt {zero} one (suc (suc ())) (s≤s le)
+ weakenPredFinLt {suc n} zero one (s≤s z≤) = z≤
+ weakenPredFinLt {suc n} zero (suc (suc l)) (s≤s le) = z≤
+ weakenPredFinLt {suc n} (suc k) (suc (suc l)) (s≤s (s≤s le)) = s≤s ( weakenPredFinLt {n} k (suc l) (s≤s le))
+
+ sucPredFin : {n : ℕ} → (k l : Fin (suc (suc n))) → toℕ k <' toℕ l → suc (predFin l) ≡ l
+ sucPredFin {zero} zero one le = refl
+ 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 →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ 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 ·
+ det (minor (predFin l) j (minor k i M))))))
+ ≡
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (toℕ i) (toℕ z) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ z) · M l (weakenFin z))
+ · det (minor (predFin l) z (minor k i M)))))
+ adjugatePropAux1a M k l le =
+ ∑∑Compat
+ (λ i j →
+ 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 ·
+ det (minor (predFin l) j (minor k i M)))))
+ (λ z z₁ →
+ ind> (toℕ z) (toℕ z₁) ·
+ (M l z · MF (toℕ k +ℕ toℕ z) ·
+ (MF (toℕ (predFin l) +ℕ toℕ z₁) · M l (weakenFin z₁))
+ · det (minor (predFin l) z₁ (minor k z M))))
+ (ind>prop
+ (λ z z₁ →
+ M l z · MF (toℕ k +ℕ toℕ z) ·
+ (MF (toℕ (predFin l) +ℕ toℕ z₁) · minor k z M (predFin l) z₁ ·
+ det (minor (predFin l) z₁ (minor k z M))))
+ (λ z z₁ →
+ M l z · MF (toℕ k +ℕ toℕ z) ·
+ (MF (toℕ (predFin l) +ℕ toℕ z₁) · M l (weakenFin z₁))
+ · det (minor (predFin l) z₁ (minor k z M)))
+ (λ i j lf →
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j ·
+ det (minor (predFin l) j (minor k i M))))
+ ≡⟨
+ cong
+ (λ a → M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · a ·
+ det (minor (predFin l) j (minor k i M))))
+ (minorSucId
+ k
+ i
+ (predFin l)
+ j
+ M
+ (weakenPredFinLt k l le)
+ lf)
+ ⟩
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · M (suc (predFin l)) (weakenFin j)
+ · det (minor (predFin l) j (minor k i M))))
+ ≡⟨ ·Assoc _ _ _ ⟩
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · M (suc (predFin l)) (weakenFin j))
+ · det (minor (predFin l) j (minor k i M)))
+ ≡⟨ cong
+ (λ a → (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · M a (weakenFin j))
+ · det (minor (predFin l) j (minor k i M))))
+ (sucPredFin
+ k
+ l
+ le
+ )
+ ⟩
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · M l (weakenFin j))
+ · det (minor (predFin l) j (minor k i M)))
+ ∎
+ )
+ )
+
+ adjugatePropAux1b : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → (k l : Fin (suc (suc n))) → toℕ k <' toℕ l →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (predFin l) j
+ · det (minor (predFin l) j (minor k (weakenFin i) M))))))
+ ≡
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ (1r + - ind> (toℕ i) (toℕ z)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc z))) · M l (suc z) ·
+ det (minor (predFin l) i (minor k (suc z) M))))))
+
+ adjugatePropAux1b M k l le =
+ ∑∑Compat
+ (λ i j →
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (predFin l) j
+ · det (minor (predFin l) j (minor k (weakenFin i) M)))))
+ (λ z z₁ →
+ (1r + - ind> (toℕ z) (toℕ z₁)) ·
+ (M l (weakenFin z) · MF (toℕ k +ℕ toℕ (weakenFin z)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc z₁))) · M l (suc z₁) ·
+ det (minor (predFin l) z (minor k (suc z₁) M)))))
+ λ i j →
+ ind>anti
+ (λ i j → (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (predFin l) j
+ · det (minor (predFin l) j (minor k (weakenFin i) M)))))
+ (λ z z₁ →
+ M l (weakenFin z) · MF (toℕ k +ℕ toℕ (weakenFin z)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc z₁))) · M l (suc z₁) ·
+ det (minor (predFin l) z (minor k (suc z₁) M))))
+ (λ i j lf →
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (predFin l) j
+ · det (minor (predFin l) j (minor k (weakenFin i) M))))
+ ≡⟨
+ cong
+ (λ a → M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · a
+ · det (minor (predFin l) j (minor k (weakenFin i) M))))
+ (minorSucSuc
+ k (weakenFin i) (predFin l) j M (weakenPredFinLt k l le) (weakenweakenFinLe i j lf))
+ ⟩
+ M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · M (suc (predFin l)) (suc j) ·
+ det (minor (predFin l) j (minor k (weakenFin i) M)))
+ ≡⟨
+ cong
+ (λ a →
+ M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · M (a) (suc j) ·
+ det (minor (predFin l) j (minor k (weakenFin i) M))))
+ (sucPredFin k l le)
+ ⟩
+ M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · M l (suc j) ·
+ det (minor (predFin l) j (minor k (weakenFin i) M)))
+ ≡⟨
+ cong
+ (λ a → M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · M l (suc j) · a))
+ (detComp
+ (minor (predFin l) j (minor k (weakenFin i) M))
+ (minor (predFin l) i (minor k (suc j) M))
+ (λ i₁ j₁ →
+ (sym (minorSemiCommR k (predFin l) j i i₁ j₁ M lf))))
+ ⟩
+ M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · M l (suc j) ·
+ det (minor (predFin l) i (minor k (suc j) M)))
+ ≡⟨ cong
+ (λ a →
+ M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (a · M l (suc j) ·
+ det (minor (predFin l) i (minor k (suc j) M))))
+ (sumMF (toℕ (predFin l)) (toℕ j))
+ ⟩
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (suc j) ·
+ det (minor (predFin l) i (minor k (suc j) M))))
+ ≡⟨
+ cong
+ (λ a → (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l)) · a · M l (suc j) ·
+ det (minor (predFin l) i (minor k (suc j) M)))))
+ (sucMFRev (toℕ j))
+ ⟩
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc j))) · M l (suc j) ·
+ det (minor (predFin l) i (minor k (suc j) M))))
+ ∎)
+ i
+ j
+
+ adjugatePropAux2a : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → (k l : Fin (suc (suc n))) →
+ toℕ k <' toℕ l →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · M l (weakenFin j))
+ · det (minor (predFin l) j (minor k i M)))))
+ ≡
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ 1r ·
+ (ind> (toℕ i) (toℕ z) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ z) · M l (weakenFin z) ·
+ det (minor (predFin l) z (minor k i M)))))))
+ adjugatePropAux2a M k l le =
+ ∑∑Compat
+ (λ i j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · M l (weakenFin j))
+ · det (minor (predFin l) j (minor k i M))))
+ (λ z z₁ →
+ 1r ·
+ (ind> (toℕ z) (toℕ z₁) ·
+ (M l z · (MF (toℕ k) · MF (toℕ z)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ z₁) · M l (weakenFin z₁) ·
+ det (minor (predFin l) z₁ (minor k z M))))))
+ (λ i j →
+ (ind> (toℕ i) (toℕ j) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · M l (weakenFin j))
+ · det (minor (predFin l) j (minor k i M))))
+ ≡⟨
+ cong
+ (λ a → (ind> (toℕ i) (toℕ j) ·
+ (M l i · a ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · M l (weakenFin j))
+ · det (minor (predFin l) j (minor k i M)))))
+ (sumMF (toℕ k) (toℕ i)) ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · M l (weakenFin j))
+ · det (minor (predFin l) j (minor k i M))))
+ ≡⟨
+ cong
+ (λ a → (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (a · M l (weakenFin j))
+ · det (minor (predFin l) j (minor k i M)))))
+ (sumMF (toℕ (predFin l)) (toℕ j))
+ ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j))
+ · det (minor (predFin l) j (minor k i M))))
+ ≡⟨ cong
+ (λ a → (ind> (toℕ i) (toℕ j) · a))
+ (sym (·Assoc _ _ _))
+ ⟩
+ ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M))))
+ ≡⟨ sym (·IdL _) ⟩
+ (1r · (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M))))))
+ ∎ )
+
+ adjugatePropAux2b : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → (k l : Fin (suc (suc n))) →
+ toℕ k <' toℕ l →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · MF (toℕ k +ℕ toℕ (weakenFin j)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (predFin l) j (minor k i M))))))
+ ≡
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ - 1r ·
+ (ind> (toℕ i) (toℕ z) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ z) · M l (weakenFin z) ·
+ det (minor (predFin l) z (minor k i M)))))))
+ adjugatePropAux2b M k l le =
+ ∑∑Compat
+ (λ i j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · MF (toℕ k +ℕ toℕ (weakenFin j)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (predFin l) j (minor k i M)))))
+ (λ z z₁ →
+ - 1r ·
+ (ind> (toℕ z) (toℕ z₁) ·
+ (M l z · (MF (toℕ k) · MF (toℕ z)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ z₁) · M l (weakenFin z₁) ·
+ det (minor (predFin l) z₁ (minor k z M))))))
+ (λ i j →
+ (ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · MF (toℕ k +ℕ toℕ (weakenFin j)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (predFin l) j (minor k i M)))))
+ ≡⟨
+ cong
+ (λ a →
+ (ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · a ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (predFin l) j (minor k i M))))))
+ (sumMF (toℕ k) (toℕ (weakenFin j)))
+ ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ (weakenFin j))) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (predFin l) j (minor k i M)))))
+ ≡⟨
+ cong
+ (λ a →
+ (ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · (MF (toℕ k) · MF a) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (predFin l) j (minor k i M))))))
+ (toℕweakenFin j) ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (predFin l) j (minor k i M)))))
+ ≡⟨
+ cong
+ (λ a → ind> (toℕ i) (toℕ j) · a)
+ (sym (·Assoc _ _ _))
+ ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) ·
+ (MF (toℕ k) · MF (toℕ j) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (predFin l) j (minor k i M))))))
+ ≡⟨
+ cong
+ (λ a →
+ ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · a))
+ (sym (·Assoc _ _ _))
+ ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) ·
+ (MF (toℕ k) ·
+ (MF (toℕ j) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (predFin l) j (minor k i M)))))))
+ ≡⟨
+ cong
+ (λ a →
+ (ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) ·
+ (MF (toℕ k) · a))))
+ (·Assoc _ _ _)
+ ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) ·
+ (MF (toℕ k) ·
+ (MF (toℕ j) · (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i)
+ · det (minor (predFin l) j (minor k i M))))))
+ ≡⟨
+ cong
+ (λ a → ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · a))
+ (·Assoc _ _ _)
+ ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) ·
+ (MF (toℕ k) ·
+ (MF (toℕ j) · (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i))
+ · det (minor (predFin l) j (minor k i M)))))
+ ≡⟨ cong
+ (λ a → ind> (toℕ i) (toℕ j) · a)
+ (·Assoc _ _ _)
+ ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) ·
+ (MF (toℕ k) ·
+ (MF (toℕ j) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i)))
+ · det (minor (predFin l) j (minor k i M))))
+ ≡⟨
+ cong
+ (λ a → ind> (toℕ i) (toℕ j) · (a · det (minor (predFin l) j (minor k i M))))
+ (solve! P')
+ ⟩
+ ind> (toℕ i) (toℕ j) ·
+ (- 1r · M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j))
+ · det (minor (predFin l) j (minor k i M)))
+ ≡⟨ ·Assoc _ _ _ ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ (- 1r · M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j)))
+ · det (minor (predFin l) j (minor k i M)))
+ ≡⟨
+ cong
+ (λ a → a · det (minor (predFin l) j (minor k i M)))
+ (·Assoc _ _ _)
+ ⟩
+ (ind> (toℕ i) (toℕ j) · (- 1r · M l i · (MF (toℕ k) · MF (toℕ i))) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j))
+ · det (minor (predFin l) j (minor k i M)))
+ ≡⟨ cong
+ (λ a → a · (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j))
+ · det (minor (predFin l) j (minor k i M)))
+ (solve! P')
+ ⟩
+ (- 1r) · ind> (toℕ i) (toℕ j) · (M l i · (MF (toℕ k) · MF (toℕ i))) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j))
+ · det (minor (predFin l) j (minor k i M))
+ ≡⟨ sym (·Assoc _ _ _) ⟩
+ - 1r · ind> (toℕ i) (toℕ j) · (M l i · (MF (toℕ k) · MF (toℕ i))) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M)))
+ ≡⟨ sym (·Assoc _ _ _) ⟩
+ (- 1r · ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M)))))
+ ≡⟨ sym (·Assoc _ _ _) ⟩
+ - 1r ·
+ (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M)))))
+ ∎)
+
+ adjugatePropRG : {n : ℕ} → (M : FinMatrix R (suc n) (suc n)) → (k l : Fin (suc n)) → toℕ k <' toℕ l →
+ ∑ (λ i → (M l i · (MF (toℕ k +ℕ toℕ i) · det (minor k i M)))) ≡ 0r
+ adjugatePropRG {zero} M zero zero ()
+ adjugatePropRG {zero} M zero (suc ()) (s≤s le)
+ adjugatePropRG {suc n} M k l le =
+ ∑ (λ i → M l i · (MF (toℕ k +ℕ toℕ i) · det (minor k i M)))
+ ≡⟨ ∑Compat
+ (λ i → M l i · (MF (toℕ k +ℕ toℕ i) · det (minor k i M)))
+ (λ i → M l i · MF (toℕ k +ℕ toℕ i) · det (minor k i M))
+ (λ i → ·Assoc _ _ _) ⟩
+ ∑ (λ i → M l i · MF (toℕ k +ℕ toℕ i) · det (minor k i M))
+ ≡⟨ ∑Compat
+ (λ i → M l i · MF (toℕ k +ℕ toℕ i) · det (minor k i M))
+ (λ i → M l i · MF (toℕ k +ℕ toℕ i) · detR (predFin l) (minor k i M))
+ (λ i →
+ cong
+ (λ a → M l i · MF (toℕ k +ℕ toℕ i) · a)
+ (sym (DetRow (predFin l) (minor k i M))))
+ ⟩
+ ∑
+ (λ i →
+ M l i · MF (toℕ k +ℕ toℕ i) · detR (predFin l) (minor k i M))
+ ≡⟨ refl ⟩
+ ∑
+ (λ i →
+ M l i · MF (toℕ k +ℕ toℕ i) ·
+ ∑
+ (λ j →
+ MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j ·
+ det (minor (predFin l) j (minor k i M))))
+ ≡⟨ ∑Compat
+ (λ i →
+ M l i · MF (toℕ k +ℕ toℕ i) ·
+ ∑
+ (λ j →
+ MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j ·
+ det (minor (predFin l) j (minor k i M))))
+ (λ i →
+ ∑
+ (λ j → M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j ·
+ det (minor (predFin l) j (minor k i M)))))
+ (λ i →
+ ∑DistR
+ (M l i · MF (toℕ k +ℕ toℕ i))
+ (λ j → MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j ·
+ det (minor (predFin l) j (minor k i M))))
+ ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j ·
+ det (minor (predFin l) j (minor k i M)))))
+ ≡⟨ ∑∑Compat
+ (λ i j →
+ M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j ·
+ det (minor (predFin l) j (minor k i M))))
+ (λ z z₁ →
+ ind> (toℕ z) (toℕ z₁) ·
+ (M l z · MF (toℕ k +ℕ toℕ z) ·
+ (MF (toℕ (predFin l) +ℕ toℕ z₁) · minor k z M (predFin l) z₁ ·
+ det (minor (predFin l) z₁ (minor k z M))))
+ +
+ (1r + - ind> (toℕ z) (toℕ z₁)) ·
+ (M l z · MF (toℕ k +ℕ toℕ z) ·
+ (MF (toℕ (predFin l) +ℕ toℕ z₁) · minor k z M (predFin l) z₁ ·
+ det (minor (predFin l) z₁ (minor k z M)))))
+ (λ i j →
+ 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 ·
+ det (minor (predFin l) j (minor k i M))))
+ )
+ ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ 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 ·
+ det (minor (predFin l) j (minor k i M))))
+ +
+ (1r + - 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 ·
+ det (minor (predFin l) j (minor k i M))))))
+ ≡⟨
+ ∑∑Split
+ (λ i j → 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 ·
+ det (minor (predFin l) j (minor k i M)))))
+ (λ i j → (1r + - 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 ·
+ det (minor (predFin l) j (minor k i M)))))
+ ⟩
+ (∑
+ (λ i →
+ ∑
+ (λ j →
+ 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 ·
+ det (minor (predFin l) j (minor k i M))))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - 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 ·
+ det (minor (predFin l) j (minor k i M)))))))
+ ≡⟨ +Compat refl (∑∑ShiftWeak λ i j →
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · minor k i M (predFin l) j ·
+ det (minor (predFin l) j (minor k i M))))) ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ 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 ·
+ det (minor (predFin l) j (minor k i M))))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (predFin l) j
+ · det (minor (predFin l) j (minor k (weakenFin i) M))))))
+ ≡⟨ +Compat refl
+ (∑∑Compat
+ (λ i j →
+ (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (predFin l) j
+ · det (minor (predFin l) j (minor k (weakenFin i) M)))))
+ (λ z z₁ →
+ (1r + - ind> (toℕ z) (toℕ z₁)) ·
+ (M l (weakenFin z) · MF (toℕ k +ℕ toℕ (weakenFin z)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ z₁) ·
+ minor k (weakenFin z) M (predFin l) z₁
+ · det (minor (predFin l) z₁ (minor k (weakenFin z) M)))))
+ (λ i j →
+ cong
+ (λ a →
+ (1r + - ind> a (toℕ j)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (predFin l) j
+ · det (minor (predFin l) j (minor k (weakenFin i) M)))))
+ (toℕweakenFin i))
+ )
+ ⟩
+ (∑
+ (λ i →
+ ∑
+ (λ j →
+ 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 ·
+ det (minor (predFin l) j (minor k i M))))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (predFin l) j
+ · det (minor (predFin l) j (minor k (weakenFin i) M)))))))
+ ≡⟨ +Compat (adjugatePropAux1a M k l le) (adjugatePropAux1b M k l le) ⟩
+ (∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (toℕ i) (toℕ z) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ z) · M l (weakenFin z))
+ · det (minor (predFin l) z (minor k i M)))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ (1r + - ind> (toℕ i) (toℕ z)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc z))) · M l (suc z) ·
+ det (minor (predFin l) i (minor k (suc z) M)))))))
+ ≡⟨ +Compat
+ refl
+ (∑Comm
+ (λ i z →
+ (1r + - ind> (toℕ i) (toℕ z)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc z))) · M l (suc z) ·
+ det (minor (predFin l) i (minor k (suc z) M)))))) ⟩
+ (∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (toℕ i) (toℕ z) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ z) · M l (weakenFin z))
+ · det (minor (predFin l) z (minor k i M)))))
+ +
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc j))) · M l (suc j) ·
+ det (minor (predFin l) i (minor k (suc j) M)))))))
+ ≡⟨ +Compat refl
+ (∑∑Compat
+ (λ j i →
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc j))) · M l (suc j) ·
+ det (minor (predFin l) i (minor k (suc j) M)))))
+ (λ z z₁ →
+ ind> (suc (toℕ z)) (toℕ z₁) ·
+ (M l (weakenFin z₁) · MF (toℕ k +ℕ toℕ (weakenFin z₁)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc z))) · M l (suc z) ·
+ det (minor (predFin l) z₁ (minor k (suc z) M)))))
+ (λ j i →
+ cong
+ (λ a → a ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc j))) · M l (suc j) ·
+ det (minor (predFin l) i (minor k (suc j) M)))))
+ (sym (ind>Suc (toℕ j) (toℕ i)))
+ )) ⟩
+ (∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (toℕ i) (toℕ z) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ z) · M l (weakenFin z))
+ · det (minor (predFin l) z (minor k i M)))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (suc (toℕ i)) (toℕ z) ·
+ (M l (weakenFin z) · MF (toℕ k +ℕ toℕ (weakenFin z)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ (suc i))) · M l (suc i) ·
+ det (minor (predFin l) z (minor k (suc i) M)))))))
+ ≡⟨ +Compat refl
+ (sym (∑∑ShiftSuc
+ (λ i z →
+ (M l (weakenFin z) · MF (toℕ k +ℕ toℕ (weakenFin z)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (predFin l) z (minor k i M))))))) ⟩
+ (∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (predFin l) +ℕ toℕ j) · M l (weakenFin j))
+ · det (minor (predFin l) j (minor k i M)))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · MF (toℕ k +ℕ toℕ (weakenFin j)) ·
+ (MF (toℕ (predFin l)) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (predFin l) j (minor k i M)))))))
+ ≡⟨ +Compat
+ (adjugatePropAux2a M k l le)
+ (adjugatePropAux2b M k l le) ⟩
+ (∑
+ (λ i →
+ ∑
+ (λ z →
+ 1r ·
+ (ind> (toℕ i) (toℕ z) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ z) · M l (weakenFin z) ·
+ det (minor (predFin l) z (minor k i M)))))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ - 1r ·
+ (ind> (toℕ i) (toℕ z) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ z) · M l (weakenFin z) ·
+ det (minor (predFin l) z (minor k i M))))))))
+ ≡⟨ sym
+ (∑∑Split
+ (λ i z →
+ 1r ·
+ (ind> (toℕ i) (toℕ z) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ z) · M l (weakenFin z) ·
+ det (minor (predFin l) z (minor k i M))))))
+ λ i z →
+ - 1r ·
+ (ind> (toℕ i) (toℕ z) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ z) · M l (weakenFin z) ·
+ det (minor (predFin l) z (minor k i M))))))
+ ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ 1r ·
+ (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M)))))
+ +
+ - 1r ·
+ (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M)))))))
+ ≡⟨ ∑∑Compat
+ (λ i j →
+ 1r ·
+ (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M)))))
+ +
+ - 1r ·
+ (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M))))))
+ (λ i j → 0r)
+ (λ i j →
+ (1r ·
+ (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M)))))
+ +
+ - 1r ·
+ (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M))))))
+ ≡⟨ sym (·DistL+ 1r (- 1r) (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M)))))) ⟩
+ ((1r + - 1r) ·
+ (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M))))))
+ ≡⟨ cong
+ (λ a → a · (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M))))))
+ (+InvR 1r)
+ ⟩
+ (0r ·
+ (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M))))))
+ ≡⟨ RingTheory.0LeftAnnihilates (CommRing→Ring P') (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (predFin l)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (predFin l) j (minor k i M))))) ⟩
+ 0r
+ ∎)
+ ⟩
+ ∑ (λ (i : Fin (suc (suc n))) → ∑ (λ (j : Fin (suc n)) → 0r))
+ ≡⟨ ∑Compat
+ (λ (i : Fin (suc (suc n))) → ∑ (λ (j : Fin (suc n)) → 0r))
+ (λ (i : Fin (suc (suc n))) → 0r)
+ (λ (i : Fin (suc (suc n))) → ∑Zero {suc n} (λ (i : Fin (suc n)) → 0r) (λ (i : Fin (suc n)) → refl)) ⟩
+ ∑ (λ (i : Fin (suc (suc n))) → 0r)
+ ≡⟨ ∑Zero (λ (i : Fin (suc (suc n))) → 0r) (λ (i : Fin (suc (suc n))) → refl) ⟩
+ 0r
+ ∎
+
+ adjugateInvRGcomponent : {n : ℕ} → (M : FinMatrix R n n) → (k l : Fin n) → toℕ l <' toℕ k → (M ⋆ adjugate M) k l ≡ (det M ∘ 𝟙) k l
+ adjugateInvRGcomponent {suc n} M k l le =
+ ∑ (λ i → M k i · (MF(toℕ l +ℕ toℕ i) · det(minor l i M)) )
+ ≡⟨ adjugatePropRG M l k le ⟩
+ 0r
+ ≡⟨ sym (RingTheory.0RightAnnihilates (CommRing→Ring P') (det M)) ⟩
+ det M · 0r
+ ≡⟨ cong (λ a → det M · a) (sym (deltaPropSym k l le)) ⟩
+ (det M ∘ 𝟙) k l
+ ∎
+
+ strongenFin : {n : ℕ} {j : Fin (suc n)} → (i : Fin (suc n)) → toℕ i <' toℕ j → Fin n
+ strongenFin {zero} {zero} i ()
+ strongenFin {zero} {suc ()} i le
+ strongenFin {suc n} {suc j} zero le = zero
+ strongenFin {suc n} {suc j} (suc i) (s≤s le) = suc (strongenFin {n} {j} i le)
+
+ strongenFinLeId : {n : ℕ} {j : Fin (suc n)} → (i : Fin (suc n)) → (le : toℕ i <' toℕ j) →
+ toℕ (strongenFin i le) <' toℕ j
+ strongenFinLeId {zero} {zero} zero ()
+ strongenFinLeId {zero} {suc ()} i le
+ strongenFinLeId {suc n} {suc j} zero (s≤s z≤) = s≤s z≤
+ strongenFinLeId {suc n} {suc j} (suc i) (s≤s le) = s≤s (strongenFinLeId {n} {j} i le)
+
+ weakenStrongenFin : {n : ℕ} {j : Fin (suc n)} → (i : Fin (suc n)) → (le : toℕ i <' toℕ j) →
+ weakenFin (strongenFin i le) ≡ i
+ weakenStrongenFin {zero} {zero} i ()
+ weakenStrongenFin {zero} {suc ()} zero le
+ weakenStrongenFin {suc n} {suc j} zero le = refl
+ weakenStrongenFin {suc n} {suc j} (suc i) (s≤s le) =
+ cong
+ (λ a → suc a)
+ (weakenStrongenFin {n} {j} i le)
+
+ toℕstrongenFin : {n : ℕ} {j : Fin (suc n)} → (i : Fin (suc n)) → (le : toℕ i <' toℕ j) →
+ toℕ (strongenFin i le) ≡ toℕ i
+ toℕstrongenFin {zero} {zero} i ()
+ toℕstrongenFin {zero} {suc ()} i (le)
+ toℕstrongenFin {suc n} {suc j} zero le = refl
+ toℕstrongenFin {suc n} {suc j} (suc i) (s≤s le) =
+ cong (λ a → suc a) (toℕstrongenFin {n} {j} i le)
+
+
+ adjugatePropAux3a : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → (k l : Fin (suc (suc n))) → (le : toℕ l <' toℕ k) →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M))))))
+ ≡
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (toℕ i) (toℕ z) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ l) · MF (toℕ z) · M l (weakenFin z) ·
+ det (minor (strongenFin l le) z (minor k i M))))))
+ adjugatePropAux3a M k l le =
+ ∑∑Compat
+ (λ i j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M)))))
+ (λ z z₁ →
+ ind> (toℕ z) (toℕ z₁) ·
+ (M l z · (MF (toℕ k) · MF (toℕ z)) ·
+ (MF (toℕ l) · MF (toℕ z₁) · M l (weakenFin z₁) ·
+ det (minor (strongenFin l le) z₁ (minor k z M)))))
+ (ind>prop
+ (λ i j →
+ M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M))))
+ (λ z z₁ →
+ M l z · (MF (toℕ k) · MF (toℕ z)) ·
+ (MF (toℕ l) · MF (toℕ z₁) · M l (weakenFin z₁) ·
+ det (minor (strongenFin l le) z₁ (minor k z M))))
+ (λ i j lf →
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M))))
+ ≡⟨
+ cong
+ (λ a →
+ M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) · a
+ · det (minor (strongenFin l le) j (minor k i M))))
+ (minorIdId
+ k
+ i
+ (strongenFin l le)
+ j
+ M
+ (strongenFinLeId l le)
+ lf)
+ ⟩
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ M (weakenFin (strongenFin l le)) (weakenFin j)
+ · det (minor (strongenFin l le) j (minor k i M))))
+ ≡⟨
+ cong
+ (λ a →
+ M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ M a (weakenFin j)
+ · det (minor (strongenFin l le) j (minor k i M))))
+ (weakenStrongenFin l le)
+ ⟩
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) · M l (weakenFin j) ·
+ det (minor (strongenFin l le) j (minor k i M))))
+ ≡⟨
+ cong
+ (λ a → M l i · a ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) · M l (weakenFin j) ·
+ det (minor (strongenFin l le) j (minor k i M))))
+ (sumMF (toℕ k) (toℕ i))
+ ⟩
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) · M l (weakenFin j) ·
+ det (minor (strongenFin l le) j (minor k i M))))
+ ≡⟨
+ cong
+ (λ a →
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (a · M l (weakenFin j) ·
+ det (minor (strongenFin l le) j (minor k i M)))))
+ (sumMF (toℕ (strongenFin l le)) (toℕ j))
+ ⟩
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ (strongenFin l le)) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (strongenFin l le) j (minor k i M))))
+ ≡⟨
+ cong
+ (λ a → M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF a · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (strongenFin l le) j (minor k i M))))
+ (toℕstrongenFin l le)
+ ⟩
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ l) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (strongenFin l le) j (minor k i M))))
+ ∎)
+ )
+
+ adjugatePropAux3b : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) → (k l : Fin (suc (suc n))) → (le : toℕ l <' toℕ k) →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k (weakenFin i) M))))))
+ ≡
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (suc (toℕ z)) (toℕ i) ·
+ (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF (toℕ l) · (- 1r · MF (suc (toℕ z))) · M l (suc z) ·
+ det (minor (strongenFin l le) i (minor k (suc z) M))))))
+ adjugatePropAux3b M k l le =
+ ∑∑Compat
+ (λ i j →
+ (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k (weakenFin i) M)))))
+ (λ z z₁ →
+ ind> (suc (toℕ z₁)) (toℕ z) ·
+ (M l (weakenFin z) · (MF (toℕ k) · MF (toℕ (weakenFin z))) ·
+ (MF (toℕ l) · (- 1r · MF (suc (toℕ z₁))) · M l (suc z₁) ·
+ det (minor (strongenFin l le) z (minor k (suc z₁) M)))))
+ (λ i j →
+ (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k (weakenFin i) M))))
+ ≡⟨ cong
+ (λ a → (1r + - ind> a (toℕ j)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k (weakenFin i) M)))))
+ (toℕweakenFin i) ⟩
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k (weakenFin i) M))))
+ ≡⟨
+ ind>anti
+ (λ i j → M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k (weakenFin i) M))))
+ (λ z z₁ →
+ M l (weakenFin z) · (MF (toℕ k) · MF (toℕ (weakenFin z))) ·
+ (MF (toℕ l) · (- 1r · MF (suc (toℕ z₁))) · M l (suc z₁) ·
+ det (minor (strongenFin l le) z (minor k (suc z₁) M))))
+ (λ i j lf →
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k (weakenFin i) M))))
+ ≡⟨
+ cong
+ (λ a →
+ M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) · a
+ · det (minor (strongenFin l le) j (minor k (weakenFin i) M))))
+ (minorIdSuc
+ k
+ (weakenFin i)
+ (strongenFin l le)
+ j
+ M
+ (strongenFinLeId l le)
+ (weakenweakenFinLe i j lf))
+ ⟩
+ M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ M (weakenFin (strongenFin l le)) (suc j)
+ · det (minor (strongenFin l le) j (minor k (weakenFin i) M)))
+ ≡⟨
+ cong
+ (λ a →
+ M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ M (weakenFin (strongenFin l le)) (suc j) · a))
+ (detComp
+ (minor (strongenFin l le) j (minor k (weakenFin i) M))
+ (minor (strongenFin l le) i (minor k (suc j) M))
+ (λ i₁ j₁ → sym
+ (minorSemiCommR k (strongenFin l le) j i i₁ j₁ M lf) )
+ )
+ ⟩
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ M (weakenFin (strongenFin l le)) (suc j)
+ · det (minor (strongenFin l le) i (minor k (suc j) M))))
+ ≡⟨
+ cong
+ (λ a →
+ M l (weakenFin i) · a ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ M (weakenFin (strongenFin l le)) (suc j)
+ · det (minor (strongenFin l le) i (minor k (suc j) M))))
+ (sumMF (toℕ k) (toℕ (weakenFin i)))
+ ⟩
+ (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ M (weakenFin (strongenFin l le)) (suc j)
+ · det (minor (strongenFin l le) i (minor k (suc j) M))))
+ ≡⟨ cong
+ (λ a → M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (a · M (weakenFin (strongenFin l le)) (suc j)
+ · det (minor (strongenFin l le) i (minor k (suc j) M))))
+ (sumMF (toℕ (strongenFin l le)) (toℕ j))
+ ⟩
+ (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF (toℕ (strongenFin l le)) · MF (toℕ j) ·
+ M (weakenFin (strongenFin l le)) (suc j)
+ · det (minor (strongenFin l le) i (minor k (suc j) M))))
+ ≡⟨
+ cong
+ (λ a →
+ M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF a · MF (toℕ j) ·
+ M (weakenFin (strongenFin l le)) (suc j)
+ · det (minor (strongenFin l le) i (minor k (suc j) M))))
+ (toℕstrongenFin l le)
+ ⟩
+ (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF (toℕ l) · MF (toℕ j) · M (weakenFin (strongenFin l le)) (suc j)
+ · det (minor (strongenFin l le) i (minor k (suc j) M))))
+ ≡⟨
+ cong
+ (λ a →
+ M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF (toℕ l) · a · M (weakenFin (strongenFin l le)) (suc j)
+ · det (minor (strongenFin l le) i (minor k (suc j) M))))
+ (sucMFRev (toℕ j))
+ ⟩
+ (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF (toℕ l) · (- 1r · MF (suc (toℕ j))) ·
+ M (weakenFin (strongenFin l le)) (suc j)
+ · det (minor (strongenFin l le) i (minor k (suc j) M))))
+ ≡⟨ cong
+ (λ a →
+ M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF (toℕ l) · (- 1r · MF (suc (toℕ j))) ·
+ M a (suc j)
+ · det (minor (strongenFin l le) i (minor k (suc j) M))))
+ (weakenStrongenFin l le)
+ ⟩
+ (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF (toℕ l) · (- 1r · MF (suc (toℕ j))) · M l (suc j) ·
+ det (minor (strongenFin l le) i (minor k (suc j) M))))
+ ∎)
+ i
+ j
+ ⟩
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF (toℕ l) · (- 1r · MF (suc (toℕ j))) · M l (suc j) ·
+ det (minor (strongenFin l le) i (minor k (suc j) M))))
+ ≡⟨
+ cong
+ (λ a →
+ a ·
+ (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF (toℕ l) · (- 1r · MF (suc (toℕ j))) · M l (suc j) ·
+ det (minor (strongenFin l le) i (minor k (suc j) M)))))
+ (sym (ind>Suc (toℕ j) (toℕ i)))
+ ⟩
+ (ind> (suc (toℕ j)) (toℕ i) ·
+ (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF (toℕ l) · (- 1r · MF (suc (toℕ j))) · M l (suc j) ·
+ det (minor (strongenFin l le) i (minor k (suc j) M)))))
+ ∎)
+
+ adjugatePropAux4a : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ (k l : Fin (suc (suc n))) → (le : toℕ l <' toℕ k) →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ l) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (strongenFin l le) j (minor k i M))))))
+ ≡
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (toℕ i) (toℕ z) ·
+ (1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ z)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin z)))
+ · det (minor (strongenFin l le) z (minor k i M)))))
+ adjugatePropAux4a M k l le =
+ ∑∑Compat
+ (λ i j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ l) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (strongenFin l le) j (minor k i M)))))
+ (λ z z₁ →
+ ind> (toℕ z) (toℕ z₁) ·
+ (1r ·
+ (M l z · (MF (toℕ k) · MF (toℕ z₁)) ·
+ (MF (toℕ l) · MF (toℕ z) · M l (weakenFin z₁)))
+ · det (minor (strongenFin l le) z₁ (minor k z M))))
+ (λ i j →
+ (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ l) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (strongenFin l le) j (minor k i M)))))
+ ≡⟨
+ cong
+ (λ a →
+ ind> (toℕ i) (toℕ j) · a)
+ (·Assoc _ _ _)
+ ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ l) · MF (toℕ j) · M l (weakenFin j))
+ · det (minor (strongenFin l le) j (minor k i M))))
+ ≡⟨
+ cong
+ (λ a →
+ ind> (toℕ i) (toℕ j) ·
+ (a · det (minor (strongenFin l le) j (minor k i M))))
+ (solve! P')
+ ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ ( 1r ·
+ ( M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) ·
+ det (minor (strongenFin l le) j (minor k i M))))
+ ∎)
+
+ adjugatePropAux4b : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ (k l : Fin (suc (suc n))) → (le : toℕ l <' toℕ k) →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ (weakenFin j))) ·
+ (MF (toℕ l) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (strongenFin l le) j (minor k i M))))))
+ ≡
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (toℕ i) (toℕ z) ·
+ (- 1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ z)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin z)))
+ · det (minor (strongenFin l le) z (minor k i M)))))
+ adjugatePropAux4b M k l le =
+ ∑∑Compat
+ (λ i j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ (weakenFin j))) ·
+ (MF (toℕ l) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (strongenFin l le) j (minor k i M)))))
+ (λ z z₁ →
+ ind> (toℕ z) (toℕ z₁) ·
+ (- 1r ·
+ (M l z · (MF (toℕ k) · MF (toℕ z₁)) ·
+ (MF (toℕ l) · MF (toℕ z) · M l (weakenFin z₁)))
+ · det (minor (strongenFin l le) z₁ (minor k z M))))
+ (λ i j →
+ (ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ (weakenFin j))) ·
+ (MF (toℕ l) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (strongenFin l le) j (minor k i M)))))
+ ≡⟨
+ cong
+ (λ a →
+ ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · (MF (toℕ k) · MF a) ·
+ (MF (toℕ l) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (strongenFin l le) j (minor k i M)))))
+ (toℕweakenFin j)
+ ⟩
+ ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (strongenFin l le) j (minor k i M))))
+ ≡⟨ cong
+ (λ a → ind> (toℕ i) (toℕ j) · a)
+ (·Assoc _ _ _)
+ ⟩
+ ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · (- 1r · MF (toℕ i)) · M l i)
+ · det (minor (strongenFin l le) j (minor k i M)))
+ ≡⟨
+ cong
+ (λ a → ind> (toℕ i) (toℕ j) · (a
+ · det (minor (strongenFin l le) j (minor k i M))))
+ (solve! P')
+ ⟩
+ ind> (toℕ i) (toℕ j) ·
+ ((- 1r) ·( M l (weakenFin j) · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l i))
+ · det (minor (strongenFin l le) j (minor k i M)))
+ ≡⟨ cong
+ (λ a → ind> (toℕ i) (toℕ j) ·
+ ((- 1r) · a
+ · det (minor (strongenFin l le) j (minor k i M))))
+ (solve! P')
+ ⟩
+ ind> (toℕ i) (toℕ j) ·
+ ((- 1r) ·
+ ( M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))) ·
+ det (minor (strongenFin l le) j (minor k i M)))
+ ∎)
+
+ adjugatePropRL : {n : ℕ} → (M : FinMatrix R (suc n) (suc n)) → (k l : Fin (suc n)) → toℕ l <' toℕ k →
+ ∑ (λ i → (M l i · (MF (toℕ k +ℕ toℕ i) · det (minor k i M)))) ≡ 0r
+ adjugatePropRL {zero} M zero zero ()
+ adjugatePropRL {zero} M (suc ()) zero (s≤s le)
+ adjugatePropRL {suc n} M k l le =
+ ∑ (λ i → M l i · (MF (toℕ k +ℕ toℕ i) · det (minor k i M)))
+ ≡⟨ ∑Compat
+ (λ i → M l i · (MF (toℕ k +ℕ toℕ i) · det (minor k i M)))
+ (λ i → M l i · MF (toℕ k +ℕ toℕ i) · det (minor k i M))
+ (λ i → ·Assoc _ _ _)
+ ⟩
+ ∑ (λ i → M l i · MF (toℕ k +ℕ toℕ i) · det (minor k i M))
+ ≡⟨ ∑Compat
+ (λ i → M l i · MF (toℕ k +ℕ toℕ i) · det (minor k i M))
+ (λ i → M l i · MF (toℕ k +ℕ toℕ i) · detR (strongenFin l le) (minor k i M))
+ (λ i →
+ cong
+ (λ a → M l i · MF (toℕ k +ℕ toℕ i) · a)
+ (sym (DetRow (strongenFin l le) (minor k i M)))) ⟩
+ ∑
+ (λ i →
+ M l i · MF (toℕ k +ℕ toℕ i) ·
+ detR (strongenFin l le) (minor k i M))
+ ≡⟨ refl ⟩
+ ∑
+ (λ i →
+ M l i · MF (toℕ k +ℕ toℕ i) ·
+ ∑
+ (λ j →
+ MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M))))
+ ≡⟨ ∑Compat
+ (λ i →
+ M l i · MF (toℕ k +ℕ toℕ i) ·
+ ∑
+ (λ j →
+ MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M))))
+ (λ i →
+ ∑
+ (λ j → M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M)))))
+ (λ i →
+ ∑DistR
+ (M l i · MF (toℕ k +ℕ toℕ i))
+ ( (λ j →
+ MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M)))))
+ ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M)))))
+ ≡⟨ ∑∑Compat
+ (λ i j →
+ M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M))))
+ (λ i j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M))))
+ +
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M)))))
+ (λ i j →
+ distributeOne
+ (ind> (toℕ i) (toℕ j))
+ ( M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M))))
+ )
+ ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M))))
+ +
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M))))))
+ ≡⟨ ∑∑Split
+ (λ i j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M)))))
+ (λ i j →
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M))))) ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M))))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M))))))
+ ≡⟨ +Compat refl (∑∑ShiftWeak (λ i j →
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M)))))) ⟩
+ (∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l i · MF (toℕ k +ℕ toℕ i) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k i M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k i M))))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) ·
+ (M l (weakenFin i) · MF (toℕ k +ℕ toℕ (weakenFin i)) ·
+ (MF (toℕ (strongenFin l le) +ℕ toℕ j) ·
+ minor k (weakenFin i) M (strongenFin l le) j
+ · det (minor (strongenFin l le) j (minor k (weakenFin i) M)))))))
+ ≡⟨ +Compat (adjugatePropAux3a M k l le) (adjugatePropAux3b M k l le) ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (toℕ i) (toℕ z) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ l) · MF (toℕ z) · M l (weakenFin z) ·
+ det (minor (strongenFin l le) z (minor k i M))))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (suc (toℕ z)) (toℕ i) ·
+ (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF (toℕ l) · (- 1r · MF (suc (toℕ z))) · M l (suc z) ·
+ det (minor (strongenFin l le) i (minor k (suc z) M))))))
+ ≡⟨ +Compat
+ refl
+ (∑Comm (λ i z →
+ ind> (suc (toℕ z)) (toℕ i) ·
+ (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF (toℕ l) · (- 1r · MF (suc (toℕ z))) · M l (suc z) ·
+ det (minor (strongenFin l le) i (minor k (suc z) M)))))) ⟩
+ (∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (toℕ i) (toℕ z) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ l) · MF (toℕ z) · M l (weakenFin z) ·
+ det (minor (strongenFin l le) z (minor k i M))))))
+ +
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ ind> (suc (toℕ j)) (toℕ i) ·
+ (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF (toℕ l) · (- 1r · MF (suc (toℕ j))) · M l (suc j) ·
+ det (minor (strongenFin l le) i (minor k (suc j) M)))))))
+ ≡⟨
+ +Compat
+ refl
+ (sym
+ (∑∑ShiftSuc
+ λ j i →
+ (M l (weakenFin i) · (MF (toℕ k) · MF (toℕ (weakenFin i))) ·
+ (MF (toℕ l) · (- 1r · MF (toℕ j)) · M l j ·
+ det (minor (strongenFin l le) i (minor k j M))))))
+ ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l i · (MF (toℕ k) · MF (toℕ i)) ·
+ (MF (toℕ l) · MF (toℕ j) · M l (weakenFin j) ·
+ det (minor (strongenFin l le) j (minor k i M))))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ i) (toℕ j) ·
+ (M l (weakenFin j) · (MF (toℕ k) · MF (toℕ (weakenFin j))) ·
+ (MF (toℕ l) · (- 1r · MF (toℕ i)) · M l i ·
+ det (minor (strongenFin l le) j (minor k i M))))))
+ ≡⟨ +Compat (adjugatePropAux4a M k l le) (adjugatePropAux4b M k l le) ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (toℕ i) (toℕ z) ·
+ (1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ z)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin z)))
+ · det (minor (strongenFin l le) z (minor k i M)))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (toℕ i) (toℕ z) ·
+ (- 1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ z)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin z)))
+ · det (minor (strongenFin l le) z (minor k i M)))))
+ ≡⟨
+ sym
+ (∑∑Split
+ (λ i z →
+ ind> (toℕ i) (toℕ z) ·
+ (1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ z)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin z)))
+ · det (minor (strongenFin l le) z (minor k i M))))
+ λ i z →
+ ind> (toℕ i) (toℕ z) ·
+ (- 1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ z)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin z)))
+ · det (minor (strongenFin l le) z (minor k i M))))
+ ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ i) (toℕ j) ·
+ (1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))
+ · det (minor (strongenFin l le) j (minor k i M)))
+ +
+ ind> (toℕ i) (toℕ j) ·
+ (- 1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))
+ · det (minor (strongenFin l le) j (minor k i M)))))
+ ≡⟨
+ ∑∑Compat
+ (λ i j →
+ ind> (toℕ i) (toℕ j) ·
+ (1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))
+ · det (minor (strongenFin l le) j (minor k i M)))
+ +
+ ind> (toℕ i) (toℕ j) ·
+ (- 1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))
+ · det (minor (strongenFin l le) j (minor k i M))))
+ (λ _ _ → 0r)
+ (λ i j →
+ (ind> (toℕ i) (toℕ j) ·
+ (1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))
+ · det (minor (strongenFin l le) j (minor k i M)))
+ +
+ ind> (toℕ i) (toℕ j) ·
+ (- 1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))
+ · det (minor (strongenFin l le) j (minor k i M))))
+ ≡⟨ sym
+ (·DistR+
+ (ind> (toℕ i) (toℕ j))
+ (1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))
+ · det (minor (strongenFin l le) j (minor k i M)))
+ (- 1r · (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))
+ · det (minor (strongenFin l le) j (minor k i M)))) ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ (1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))
+ · det (minor (strongenFin l le) j (minor k i M))
+ +
+ - 1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))
+ · det (minor (strongenFin l le) j (minor k i M)))
+ )
+ ≡⟨
+ cong
+ (λ a → ind> (toℕ i) (toℕ j) · a)
+ (sym
+ (·DistL+
+ (1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))))
+ ( - 1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))))
+ (det (minor (strongenFin l le) j (minor k i M)))))
+ ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ ((1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))
+ +
+ - 1r ·
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j))))
+ · det (minor (strongenFin l le) j (minor k i M))))
+ ≡⟨
+ cong
+ (λ a →
+ ind> (toℕ i) (toℕ j) · (a ·
+ det (minor (strongenFin l le) j (minor k i M))))
+ (sym
+ (·DistL+
+ 1r
+ (- 1r)
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))))
+ ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ ((1r + - 1r) ·
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))
+ · det (minor (strongenFin l le) j (minor k i M))))
+ ≡⟨ cong
+ (λ a → (ind> (toℕ i) (toℕ j) ·
+ (a · (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))
+ · det (minor (strongenFin l le) j (minor k i M)))))
+ (+InvR 1r)
+ ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ (0r ·
+ (M l i · (MF (toℕ k) · MF (toℕ j)) ·
+ (MF (toℕ l) · MF (toℕ i) · M l (weakenFin j)))
+ · det (minor (strongenFin l le) j (minor k i M))))
+ ≡⟨
+ cong
+ (λ a → (ind> (toℕ i) (toℕ j) ·
+ (a · det (minor (strongenFin l le) j (minor k i M)))))
+ (solve! P')
+ ⟩
+ (ind> (toℕ i) (toℕ j) ·
+ (0r · det (minor (strongenFin l le) j (minor k i M))))
+ ≡⟨ cong
+ (λ a → ind> (toℕ i) (toℕ j) · a)
+ (RingTheory.0LeftAnnihilates
+ (CommRing→Ring P')
+ (det (minor (strongenFin l le) j (minor k i M)))) ⟩
+ (ind> (toℕ i) (toℕ j) · 0r)
+ ≡⟨ solve! P' ⟩
+ 0r
+ ∎)⟩
+ ∑ (λ (i : Fin (suc (suc n))) → ∑ (λ (j : Fin (suc n)) → 0r))
+ ≡⟨ ∑Zero
+ (λ (i : Fin (suc (suc n))) → ∑ (λ (j : Fin (suc n)) → 0r))
+ (λ i → ∑Zero (λ (j : Fin (suc n)) → 0r) (λ (j : Fin (suc n)) → refl)) ⟩
+ 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)) )
+ ≡⟨ adjugatePropRL M l k le ⟩
+ 0r
+ ≡⟨ sym (RingTheory.0RightAnnihilates (CommRing→Ring P') (det M)) ⟩
+ det M · 0r
+ ≡⟨ 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
+ FinCompare {suc n} zero (suc l) = inr (inl (s≤s z≤))
+ FinCompare {suc n} (suc k) zero = inr (inr (s≤s z≤))
+ FinCompare {suc n} (suc k) (suc l) with FinCompare {n} k l
+ ... | inl x = inl (cong (λ a → (suc a)) x)
+ ... | 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
+ ... | inl x =
+ (∑ (λ i → M k i · (MF(toℕ l +ℕ toℕ i) · det(minor l i M)) )
+ ≡⟨
+ ∑Compat
+ (λ i → M k i · (MF(toℕ l +ℕ toℕ i) · det(minor l i M)))
+ (λ i → M k i · MF(toℕ l +ℕ toℕ i) · det(minor l i M))
+ (λ i → ·Assoc _ _ _)
+ ⟩
+ ∑ (λ i → M k i · MF (toℕ l +ℕ toℕ i) · det (minor l i M))
+ ≡⟨
+ ∑Compat
+ (λ i → M k i · MF (toℕ l +ℕ toℕ i) · det (minor l i M))
+ (λ i → M l i · MF (toℕ l +ℕ toℕ i) · det (minor l i M))
+ (λ i → cong
+ (λ a → M a i · MF (toℕ l +ℕ toℕ i) · det (minor l i M))
+ x )
+ ⟩
+ ∑ (λ i → M l i · MF (toℕ l +ℕ toℕ i) · det (minor l i M))
+ ≡⟨ ∑Compat
+ (λ i → M l i · MF (toℕ l +ℕ toℕ i) · det (minor l i M))
+ (λ i → MF (toℕ l +ℕ toℕ i) · M l i · det (minor l i M))
+ (λ i → cong
+ (λ a → a · det (minor l i M))
+ (CommRingStr.·Comm (snd P') (M l i) (MF (toℕ l +ℕ toℕ i))) ) ⟩
+ detR l M
+ ≡⟨ DetRow l M ⟩
+ det M
+ ≡⟨ sym (·IdR (det M)) ⟩
+ (det M · 1r)
+ ≡⟨ cong (λ a → det M · a) (sym (deltaPropEq k l x))⟩
+ (det M ∘ 𝟙) k l
+ ∎)
+ ... | 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
+ ≡⟨ refl ⟩
+ ∑ (λ i → adjugate M k i · (M ᵗ) l i)
+ ≡⟨
+ ∑Compat
+ (λ i → adjugate M k i · (M ᵗ) l i)
+ (λ i → adjugate (M ᵗ) i k · (M ᵗ) l i)
+ (λ i → cong (λ a → a · (M ᵗ) l i) (sym (adjugateTransp M i k)))
+ ⟩
+ ∑ (λ i → adjugate (M ᵗ) i k · (M ᵗ) l i)
+ ≡⟨
+ ∑Compat
+ (λ i → adjugate (M ᵗ) i k · (M ᵗ) l i)
+ (λ z → (snd P' CommRingStr.· (M ᵗ) l z) (adjugate (M ᵗ) z k))
+ (λ i → CommRingStr.·Comm (snd P') (adjugate (M ᵗ) i k) ((M ᵗ) l i))
+ ⟩
+ ∑ (λ i → (M ᵗ) l i · adjugate (M ᵗ) i k )
+ ≡⟨ adjugateInvRComp (M ᵗ) l k ⟩
+ (det (M ᵗ) ∘ 𝟙) l k
+ ≡⟨ cong (λ a → (a ∘ 𝟙) l k) (sym (detTransp M)) ⟩
+ det M · δ l k
+ ≡⟨ cong (λ a → det M · a) (deltaComm l k) ⟩
+ (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/Base.agda b/Cubical/Algebra/Determinat/Base.agda
new file mode 100644
index 000000000..e45c0baf8
--- /dev/null
+++ b/Cubical/Algebra/Determinat/Base.agda
@@ -0,0 +1,2500 @@
+{-# OPTIONS --cubical #-}
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.Determinat.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Algebra.Matrix
+open import Cubical.Algebra.Matrix.CommRingCoefficient
+open import Cubical.Data.Bool
+open import Cubical.Foundations.Structure using (⟨_⟩)
+open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_
+ ; +-comm to +ℕ-comm
+ ; +-assoc to +ℕ-assoc
+ ; ·-assoc to ·ℕ-assoc)
+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.Algebra.Semiring
+open import Cubical.Data.Int.Base using (pos; negsuc)
+open import Cubical.Data.Vec.Base using (_∷_; [])
+open import Cubical.Data.Nat.Order
+open import Cubical.Tactics.CommRingSolver
+open import Cubical.Algebra.Determinat.Minor
+open import Cubical.Algebra.Determinat.RingSum
+
+module Determinat (ℓ : Level) (P' : CommRing ℓ) where
+
+ open Cubical.Algebra.Determinat.Minor.Minor ℓ
+ open Cubical.Algebra.Determinat.RingSum.RingSum ℓ P'
+ open RingStr (snd (CommRing→Ring P')) renaming ( is-set to isSetR )
+
+ CommRingR' : CommRingStr (R' .fst)
+ CommRingR' = commringstr 0r 1r _+_ _·_ -_ (CommRingStr.isCommRing (snd P'))
+
+ -- Definition of the minor factor
+ MF : (i : ℕ) → R
+ MF zero = 1r
+ MF (suc i) = (- 1r) · (MF i)
+
+ --Properties of the minor factor
+ sumMF : (i j : ℕ) → MF (i +ℕ j) ≡ (MF i) · (MF j)
+ sumMF zero j =
+ MF j
+ ≡⟨ sym (·IdL (MF j)) ⟩
+ 1r · (MF j)
+ ≡⟨ refl ⟩
+ (MF zero) · (MF j)∎
+ sumMF (suc i) j =
+ MF (suc i +ℕ j)
+ ≡⟨ refl ⟩
+ ((- 1r) · (MF (i +ℕ j)))
+ ≡⟨ cong (λ x → (- 1r) · x) (sumMF i j) ⟩
+ ((- 1r) · ((MF i) · (MF j)))
+ ≡⟨ ·Assoc _ _ _ ⟩
+ ((- 1r) · (MF i)) · (MF j)
+ ∎
+
+ 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
+ ≡⟨ cong (λ x → x + c) eq1 ⟩
+ b + c
+ ≡⟨ 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
+ det {zero} M = 1r
+ det {suc n} M = ∑ (λ j → (MF (toℕ j)) · (M zero j) · det {n} (minor zero j M))
+
+ detComp : {n : ℕ} → (M N : FinMatrix R n n) → ((i j : Fin n) → M i j ≡ N i j ) → det M ≡ det N
+ detComp {zero} M N f = refl
+ detComp {suc n} M N f =
+ ∑ (λ j → MF (toℕ j) · M zero j · det (minor zero j M))
+ ≡⟨ ∑Compat (λ j → (MF (toℕ j)) · (M zero j) · det (minor zero j M))
+ (λ j → (MF (toℕ j)) · (N zero j) · det (minor zero j M))
+ (λ j → cong (λ a → (MF (toℕ j)) · a · det (minor zero j M)) (f zero j)) ⟩
+ ∑ (λ j → MF (toℕ j) · N zero j · det (minor zero j M))
+ ≡⟨ ∑Compat (λ j → (MF (toℕ j)) · (N zero j) · det (minor zero j M))
+ (λ j → (MF (toℕ j)) · (N zero j) · det (minor zero j N))
+ (λ j → cong (λ a → (MF (toℕ j)) · (N zero j) · a) (detComp (minor zero j M) (minor zero j N) (minorComp zero j M N f)) ) ⟩
+ ∑ (λ j → MF (toℕ j) · N zero j · det (minor zero j N)) ∎
+
+ -- Independence of the row in the Laplace expansion.
+ detR : ∀ {n} → (k : Fin n) → FinMatrix R n n → R
+ detR {suc n} k M = ∑ (λ j → (MF ((toℕ k) +ℕ (toℕ j))) · (M k j) · det {n} (minor k j M))
+
+ DetRowAux1 : {n : ℕ} →
+ (k i : Fin (suc (suc n))) →
+ (j : Fin (suc n)) →
+ (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ MF ((toℕ k) +ℕ (toℕ i)) · M k i ·
+ (MF (toℕ j) · minor k i M zero j ·
+ det (minor zero j (minor k i M)))
+ ≡
+ ( MF ((toℕ k) +ℕ (toℕ i) +ℕ (toℕ j)) ·
+ M k i · minor k i M zero j ·
+ det (minor zero j (minor k i M)))
+ DetRowAux1 k i j M =
+ (MF (toℕ k +ℕ toℕ i) · M k i ·
+ (MF (toℕ j) · minor k i M zero j ·
+ det (minor zero j (minor k i M))))
+ ≡⟨
+ ·Assoc
+ ( MF ((toℕ k) +ℕ (toℕ i)) · M k i)
+ (MF (toℕ j) · minor k i M zero j)
+ ( det (minor zero j (minor k i M)))
+ ⟩
+ (MF (toℕ k +ℕ toℕ i) · M k i · (MF (toℕ j) · minor k i M zero j) ·
+ det (minor zero j (minor k i M)))
+ ≡⟨
+ cong
+ (λ x → (x · det (minor zero j (minor k i M))))
+ (·Assoc
+ ( MF ((toℕ k) +ℕ (toℕ i)) · M k i)
+ (MF (toℕ j))
+ ( minor k i M zero j))
+ ⟩
+ (MF (toℕ k +ℕ toℕ i) · M k i · MF (toℕ j) · minor k i M zero j ·
+ det (minor zero j (minor k i M)))
+ ≡⟨
+ cong
+ (λ x → x · minor k i M zero j · det (minor zero j (minor k i M)))
+ (sym (·Assoc (MF ((toℕ k) +ℕ (toℕ i))) ( M k i ) (MF (toℕ j))))
+ ⟩
+ (MF (toℕ k +ℕ toℕ i) · (M k i · MF (toℕ j)) · minor k i M zero j ·
+ det (minor zero j (minor k i M)))
+ ≡⟨
+ cong
+ ( λ x →
+ MF ((toℕ k) +ℕ (toℕ i)) · x ·
+ minor k i M zero j ·
+ det (minor zero j (minor k i M)))
+ (CommRingStr.·Comm CommRingR' (M k i) ( MF (toℕ j)))
+ ⟩
+ MF (toℕ k +ℕ toℕ i) · (MF (toℕ j) · M k i)
+ · minor k i M zero j
+ · det (minor zero j (minor k i M))
+ ≡⟨
+ cong
+ (λ x →
+ x · minor k i M zero j · det (minor zero j (minor k i M)))
+ (·Assoc (MF ((toℕ k) +ℕ (toℕ i))) ( MF (toℕ j)) (M k i))
+ ⟩
+ (MF (toℕ k +ℕ toℕ i) · MF (toℕ j) · M k i · minor k i M zero j ·
+ det (minor zero j (minor k i M)))
+ ≡⟨
+ cong
+ (λ x →
+ x · M k i · minor k i M zero j
+ · det (minor zero j (minor k i M)))
+ (sym (sumMF (toℕ k +ℕ toℕ i) ( toℕ j)))
+ ⟩
+ (MF (toℕ k +ℕ toℕ i +ℕ toℕ j) · M k i · minor k i M zero j ·
+ det (minor zero j (minor k i M)))
+ ∎
+
+ DetRowAux3a :
+ {n : ℕ} → (k : Fin (suc n)) →
+ (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ ∑ (λ (i : Fin (suc (suc n))) →
+ ∑ (λ (j : Fin (suc n)) →
+ 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)))))
+ ≡
+ ∑ (λ (i : Fin (suc n)) →
+ ∑ (λ (j : Fin (suc n)) →
+ ind> (toℕ (suc i)) (toℕ j) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j)
+ · M (suc k) (suc i) · minor (suc k) (suc i) M zero j
+ · det (minor zero j (minor (suc k) (suc i) M)))))
+ DetRowAux3a k M =
+ ∑∑ShiftSuc
+ (λ i 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))))
+
+ DetRowAux3b : {n : ℕ} → (k : Fin (suc n)) →
+ (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - 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)))))
+ ≡
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) · M (suc k) (weakenFin i) ·
+ minor (suc k) (weakenFin i) M zero j
+ · det (minor zero j (minor (suc k) (weakenFin i) M)))))
+ DetRowAux3b k M =
+ ∑∑ShiftWeak
+ (λ i 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))))
+
+ DetRowAux4a : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ ∑ (λ i →
+ ∑ (λ j →
+ ind> (toℕ (suc i)) (toℕ j) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ minor (suc k) (suc i) M zero j
+ · det (minor zero j (minor (suc k) (suc i) M)))))
+ ≡
+ ∑ (λ i →
+ ∑ (λ j →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M)))))
+ DetRowAux4a k M =
+ ∑∑Compat
+ (λ i j →
+ ind> (toℕ (suc i)) (toℕ j) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ minor (suc k) (suc i) M zero j
+ · det (minor zero j (minor (suc k) (suc i) M))))
+ (λ i j → (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M))))
+ λ i j →
+ (
+ ind> (toℕ (suc i)) (toℕ j) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ minor (suc k) (suc i) M zero j
+ · det (minor zero j (minor (suc k) (suc i) M)))
+ ≡⟨
+ cong
+ (λ a →
+ a ·(MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j)
+ · M (suc k) (suc i) · minor (suc k) (suc i) M zero j
+ · det (minor zero j (minor (suc k) (suc i) M))))
+ (ind>Suc (toℕ i) (toℕ j))
+ ⟩
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ minor (suc k) (suc i) M zero j
+ · det (minor zero j (minor (suc k) (suc i) M)))
+ ≡⟨ ind>anti
+ (λ j i →
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ minor (suc k) (suc i) M zero j
+ · det (minor zero j (minor (suc k) (suc i) M))))
+ (λ j i →
+ MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M)))
+ (λ j i le →
+ (
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ minor (suc k) (suc i) M zero j
+ · det (minor zero j (minor (suc k) (suc i) M)))
+ ≡⟨
+ cong
+ (λ a →
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j)
+ · M (suc k) (suc i)
+ · a
+ · det (minor zero j (minor (suc k) (suc i) M))))
+ (minorIdId (suc k) (suc i) zero j M (s≤s z≤) (s≤s le))
+ ⟩
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor zero j (minor (suc k) (suc i) M)))
+ ≡⟨ cong
+ (λ a →
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero (weakenFin j) · a))
+ (detComp
+ (minor zero j (minor (suc k) (suc i) M))
+ (minor k i (minor (weakenFin zero) (weakenFin j) M))
+ λ i₁ j₁ →
+ minorComm0 k zero i j i₁ j₁ M z≤ le )
+ ⟩
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M)))
+ ∎
+ )
+ )
+ j
+ i ⟩
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M)))
+ ∎)
+
+ toℕweakenFin : {n : ℕ} → (i : Fin n) → toℕ (weakenFin i) ≡ toℕ i
+ toℕweakenFin zero = refl
+ toℕweakenFin (suc i) = cong suc (toℕweakenFin i)
+
+ weakenweakenFinLe : {n : ℕ} → (i : Fin (suc n)) → (j : Fin (suc n)) → toℕ i ≤' toℕ j → weakenFin i ≤'Fin weakenFin j
+ weakenweakenFinLe {zero} zero zero le = le
+ weakenweakenFinLe {suc n} zero zero le = le
+ weakenweakenFinLe {suc n} zero (suc j) le = z≤
+ weakenweakenFinLe {suc n} (suc i) (suc j) (s≤s le) = s≤s (weakenweakenFinLe {n} i j le)
+
+ DetRowAux4b : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · minor (suc k) (weakenFin i) M zero j
+ · det (minor zero j (minor (suc k) (weakenFin i) M)))))
+ ≡
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (ind> (suc (toℕ j)) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M))))))
+ DetRowAux4b k M =
+ ∑∑Compat
+ (λ i j →
+ (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · minor (suc k) (weakenFin i) M zero j
+ · det (minor zero j (minor (suc k) (weakenFin i) M))))
+ (λ z z₁ →
+ ind> (suc (toℕ z₁)) (toℕ z) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin z) +ℕ toℕ z₁) ·
+ M (suc k) (weakenFin z)
+ · M (weakenFin zero) (suc z₁)
+ · det (minor k z (minor zero (suc z₁) M))))
+ λ i j →
+ (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · minor (suc k) (weakenFin i) M zero j
+ · det (minor zero j (minor (suc k) (weakenFin i) M)))
+ ≡⟨
+ cong
+ (λ a →
+ (1r + - ind> a (toℕ j)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · minor (suc k) (weakenFin i) M zero j
+ · det (minor zero j (minor (suc k) (weakenFin i) M))))
+ (toℕweakenFin i)
+ ⟩
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · minor (suc k) (weakenFin i) M zero j
+ · det (minor zero j (minor (suc k) (weakenFin i) M)))
+ ≡⟨ ind>anti
+ (λ i j → (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · minor (suc k) (weakenFin i) M zero j
+ · det (minor zero j (minor (suc k) (weakenFin i) M))))
+ (λ i j → MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M)))
+ (λ i j le →
+ ((MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · minor (suc k) (weakenFin i) M zero j
+ · det (minor zero j (minor (suc k) (weakenFin i) M))))
+ ≡⟨ cong
+ (λ a →
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i) · a
+ · det (minor zero j (minor (suc k) (weakenFin i) M))))
+ (minorIdSuc
+ (suc k)
+ (weakenFin i)
+ zero
+ j
+ M
+ (s≤s z≤)
+ (weakenweakenFinLe i j le)) ⟩
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor zero j (minor (suc k) (weakenFin i) M)))
+ ≡⟨ cong
+ (λ a →
+ MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j) · a)
+ (detComp
+ (minor zero j (minor (suc k) (weakenFin i) M))
+ (minor k i (minor zero (suc j) M))
+ (λ i₁ j₁ →
+ minorComm1 k zero i j i₁ j₁ M z≤ le))
+ ⟩
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M)))
+ ∎)
+ i
+ j ⟩
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M)))
+ ≡⟨ cong
+ (λ a →
+ a · (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M))))
+ (sym (ind>Suc (toℕ j) (toℕ i)))
+ ⟩
+ (ind> (suc (toℕ j)) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M))))
+ ∎
+
+
+ DetRowAux5a : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M)))))
+ ≡
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M)))))
+ DetRowAux5a k M = ∑Comm λ i j → (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M)))
+
+ DetRowAux5b : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (suc (toℕ j)) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M)))))
+ ≡
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ ind> (suc (toℕ j)) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M)))))
+ DetRowAux5b k M =
+ ∑Comm (λ i j →
+ ind> (suc (toℕ j)) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M))))
+
+ DetRowAux6a : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M)))))
+ ≡
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero j
+ · det (minor k i (minor zero j M)))))
+ DetRowAux6a k M =
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M)))))
+ ≡⟨ ∑∑Compat
+ (λ j i →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M))))
+ (λ j i →
+ (1r + - ind> (toℕ (weakenFin j)) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ (weakenFin j)) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M))))
+ (λ j i →
+ cong (λ a →
+ (1r + - ind> a (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ a) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M))))
+ (sym (toℕweakenFin j)))
+ ⟩
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ (1r + - ind> (toℕ (weakenFin j)) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ (weakenFin j)) ·
+ M (suc k) (suc i)
+ · M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M)))))
+ ≡⟨ sym (∑∑ShiftWeak
+ λ j i →
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) ·
+ M (suc k) (suc i)
+ · M zero j
+ · det (minor k i (minor zero j M)))) ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc j) +ℕ toℕ i) · M (suc k) (suc j) ·
+ M zero i
+ · det (minor k j (minor zero i M)))))
+ ∎
+
+ DetRowAux6bAux : {n : ℕ} → (k : Fin (suc n)) → (i j : Fin (suc n)) →
+ MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j)
+ ≡
+ MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ (suc j))
+ DetRowAux6bAux k i j =
+ MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j)
+ ≡⟨ sumMF (toℕ (suc k) +ℕ toℕ (weakenFin i)) (toℕ j) ⟩
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i)) · MF (toℕ j))
+ ≡⟨ cong
+ (λ a →
+ a · MF (toℕ j))
+ (sumMF (toℕ (suc k)) (toℕ (weakenFin i)))
+ ⟩
+ (MF (toℕ (suc k)) · MF (toℕ (weakenFin i)) · MF (toℕ j))
+ ≡⟨ cong
+ (λ a →
+ MF (toℕ (suc k)) · (MF a ) · MF (toℕ j))
+ (toℕweakenFin i)
+ ⟩
+ (MF (toℕ (suc k)) · MF (toℕ i) · MF (toℕ j))
+ ≡⟨ sym
+ (·Assoc
+ (MF (toℕ (suc k)))
+ (MF (toℕ i))
+ (MF (toℕ j)))
+ ⟩
+ (MF (toℕ (suc k)) · (MF (toℕ i) · MF (toℕ j)))
+ ≡⟨ cong
+ (λ a →
+ MF (toℕ (suc k)) · a)
+ (solve! P') ⟩
+ MF (toℕ (suc k)) · (MF (toℕ (suc i)) · MF (toℕ (suc j)))
+ ≡⟨
+ ·Assoc
+ (MF (toℕ (suc k)))
+ (MF (toℕ (suc i)))
+ (MF (toℕ (suc j)))
+ ⟩
+ (MF (toℕ (suc k)) · MF (toℕ (suc i)) · MF (toℕ (suc j)))
+ ≡⟨ cong
+ (λ a → a · MF (toℕ (suc j)))
+ (sym (sumMF (toℕ (suc k)) (toℕ (suc i))))
+ ⟩
+ (MF (toℕ (suc k) +ℕ toℕ (suc i)) · MF (toℕ (suc j)))
+ ≡⟨ sym (sumMF (toℕ (suc k) +ℕ toℕ (suc i)) (toℕ (suc j))) ⟩
+ MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ (suc j))
+ ∎
+
+ DetRowAux6b : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ ind> (suc (toℕ j)) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M)))))
+ ≡
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ ind> (toℕ j) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (weakenFin i)
+ · M zero j
+ · det (minor k i (minor zero j M)))))
+
+ DetRowAux6b k M =
+ ∑
+ (λ i →
+ ∑
+ (λ i₁ →
+ ind> (suc (toℕ i)) (toℕ i₁) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i₁) +ℕ toℕ i) ·
+ M (suc k) (weakenFin i₁)
+ · M (weakenFin zero) (suc i)
+ · det (minor k i₁ (minor zero (suc i) M)))))
+ ≡⟨ ∑∑Compat
+ (λ j i →
+ ind> (suc (toℕ j)) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M))))
+ (λ j i →
+ ind> (suc (toℕ j)) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ (suc j)) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M))))
+ (λ j i →
+ (ind> (suc (toℕ j)) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M))))
+ ≡⟨ cong
+ (λ a →
+ ind> (suc (toℕ j)) (toℕ i) ·
+ (a ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M))))
+ (DetRowAux6bAux k i j)
+ ⟩
+ (ind> (suc (toℕ j)) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ (suc j)) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M))))
+ ∎)
+ ⟩
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ ind> (suc (toℕ j)) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ (suc j)) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M)))))
+ ≡⟨ sym (∑∑ShiftSuc λ j i → (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) j
+ · det (minor k i (minor zero j M)))) ⟩
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ ind> (toℕ j) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M zero j
+ · det (minor k i (minor zero j M)))))
+ ∎
+
+ weakenFinLe : {n : ℕ} → (i : Fin (suc (suc n))) → (j : Fin (suc n)) → toℕ i ≤' toℕ j → i ≤'Fin weakenFin j
+ weakenFinLe {zero} zero zero le = le
+ weakenFinLe {zero} one zero ()
+ weakenFinLe {zero} one (suc ()) le
+ weakenFinLe {suc n} zero j le = z≤
+ weakenFinLe {suc n} (suc i) (suc j) (s≤s le) = s≤s (weakenFinLe {n} i j le)
+
+ DetRowAux7a : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero j
+ · det (minor k i (minor zero j M)))))
+ ≡
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i ·
+ M zero j
+ · det (minor k i (minor zero j M)))))
+
+ DetRowAux7a k M =
+ ∑∑Compat
+ (λ j i →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero j
+ · det (minor k i (minor zero j M))))
+ (λ j i →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i ·
+ M zero j
+ · det (minor k i (minor zero j M))))
+ (λ j i →
+ ind>anti
+ (λ j i → (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero j
+ · det (minor k i (minor zero j M))))
+ (λ j i → (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i ·
+ M zero j
+ · det (minor k i (minor zero j M))))
+ (λ j i le →
+ cong
+ ( λ a → MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · a ·
+ M zero j
+ · det (minor k i (minor zero j M)))
+ (sym (minorSucSuc zero j k i M z≤ (weakenFinLe j i le))))
+ j
+ i)
+
+ DetRowAux7b : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ ind> (toℕ j) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (weakenFin i)
+ · M zero j
+ · det (minor k i (minor zero j M)))))
+ ≡
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ ind> (toℕ j) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i ·
+ M zero j
+ · det (minor k i (minor zero j M)))))
+ DetRowAux7b k M =
+ ∑∑Compat
+ (λ j i →
+ ind> (toℕ j) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (weakenFin i)
+ · M zero j
+ · det (minor k i (minor zero j M))))
+ (λ j i →
+ (ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i ·
+ M zero j
+ · det (minor k i (minor zero j M))))
+ (λ j i →
+ ind>prop
+ (λ j i →
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (weakenFin i) ·
+ M zero j · det (minor k i (minor zero j M))))
+ (λ j i →
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i ·
+ M zero j
+ · det (minor k i (minor zero j M))))
+ (λ j i le →
+ cong
+ (λ a →
+ MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · a ·
+ M zero j · det (minor k i (minor zero j M)))
+ (sym (minorSucId zero j k i M z≤ le)) )
+ j
+ i
+ )
+
+ DetRowAux8 : {n : ℕ} → (i : Fin (suc (suc n))) → (j k : Fin (suc n))
+ → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ 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))
+ ≡
+ MF (toℕ i) · M zero i · (MF (toℕ k +ℕ toℕ j) · minor zero i M k j · det (minor k j (minor zero i M)))
+ DetRowAux8 i j k M =
+ (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)))
+ ≡⟨ cong
+ (λ a →
+ a · minor zero i M k j · M zero i · det (minor k j (minor zero i M)))
+ (sumMF (toℕ (suc k) +ℕ toℕ (suc j)) ( toℕ i))
+ ⟩
+ (MF (toℕ (suc k) +ℕ toℕ (suc j)) · MF (toℕ i) · minor zero i M k j ·
+ M zero i
+ · det (minor k j (minor zero i M)))
+ ≡⟨ cong
+ (λ a → a · MF (toℕ i) · minor zero i M k j ·
+ M zero i
+ · det (minor k j (minor zero i M)))
+ (sumMF (toℕ (suc k)) (toℕ (suc j)))
+ ⟩
+ (MF (toℕ (suc k)) · MF (toℕ (suc j)) · MF (toℕ i) ·
+ minor zero i M k j
+ · M zero i
+ · det (minor k j (minor zero i M)))
+ ≡⟨ cong
+ (λ a →
+ a · MF (toℕ i) ·
+ minor zero i M k j
+ · M zero i
+ · det (minor k j (minor zero i M)))
+ (solve! P')
+ ⟩
+ MF (toℕ k) · MF (toℕ j) · MF (toℕ i) ·
+ minor zero i M k j
+ · M zero i
+ · det (minor k j (minor zero i M))
+ ≡⟨ cong
+ (λ a →
+ a · MF (toℕ i) · minor zero i M k j
+ · M zero i · det (minor k j (minor zero i M)))
+ (sym (sumMF (toℕ k) (toℕ j))) ⟩
+ (MF (toℕ k +ℕ toℕ j) · MF (toℕ i) · minor zero i M k j · M zero i ·
+ det (minor k j (minor zero i M)))
+ ≡⟨ cong
+ (λ a → a · det (minor k j (minor zero i M)))
+ (solve! P')
+ ⟩
+ ( MF (toℕ i) · M zero i · MF (toℕ k +ℕ toℕ j) · minor zero i M k j ·
+ det (minor k j (minor zero i M)))
+ ≡⟨ sym
+ (·Assoc
+ (MF (toℕ i) · M zero i · MF (toℕ k +ℕ toℕ j))
+ (minor zero i M k j)
+ (det (minor k j (minor zero i M))))
+ ⟩
+ (MF (toℕ i) · M zero i · MF (toℕ k +ℕ toℕ j) ·
+ (minor zero i M k j · det (minor k j (minor zero i M))))
+ ≡⟨ sym (·Assoc (MF (toℕ i) · M zero i) (MF (toℕ k +ℕ toℕ j)) (minor zero i M k j · det (minor k j (minor zero i M)))) ⟩
+ MF (toℕ i) · M zero i · (MF (toℕ k +ℕ toℕ j) ·
+ (minor zero i M k j · det (minor k j (minor zero i M))))
+ ≡⟨ cong
+ (λ a → MF (toℕ i) · M zero i · a)
+ (·Assoc (MF (toℕ k +ℕ toℕ j)) (minor zero i M k j) (det (minor k j (minor zero i M)))) ⟩
+ (MF (toℕ i) · M zero i · (MF (toℕ k +ℕ toℕ j) ·
+ minor zero i M k j · det (minor k j (minor zero i M))))
+ ∎
+
+
+ DetRow : ∀ {n} → (k : Fin n) → (M : FinMatrix R n n) → (detR k M) ≡ (det M)
+ DetRow {one} zero M = refl
+ DetRow {suc (suc n)} zero M = refl
+ DetRow {suc (suc n)} (suc k) M =
+ detR (suc k) M
+ ≡⟨ refl ⟩
+ ∑
+ (λ (i : Fin (suc (suc n))) →
+ MF (toℕ (suc k) +ℕ toℕ i) · M (suc k) i · det (minor (suc k) i M))
+ ≡⟨ refl ⟩
+ ∑
+ (λ i →
+ MF (toℕ (suc k) +ℕ toℕ i) · M (suc k) i ·
+ ∑
+ (λ j →
+ MF (toℕ j) · minor (suc k) i M zero j ·
+ det (minor zero j (minor (suc k) i M))))
+ ≡⟨ ∑Compat (λ i →
+ MF (toℕ (suc k) +ℕ toℕ i) · M (suc k) i ·
+ ∑
+ (λ j →
+ MF (toℕ j) · minor (suc k) i M zero j ·
+ det (minor zero j (minor (suc k) i M))))
+ ((λ i →
+ ∑
+ (λ j →
+ MF (toℕ (suc k) +ℕ toℕ i) · M (suc k) i ·
+ (MF (toℕ j) · minor (suc k) i M zero j ·
+ det (minor zero j (minor (suc k) i M))))))
+ (λ i → ∑DistR ( MF (toℕ (suc k) +ℕ toℕ i) · M (suc k) i)
+ (λ j →
+ MF (toℕ j) · minor (suc k) i M zero j ·
+ det (minor zero j (minor (suc k) i M))))⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ MF (toℕ (suc k) +ℕ toℕ i) · M (suc k) i ·
+ (MF (toℕ j) · minor (suc k) i M zero j ·
+ det (minor zero j (minor (suc k) i M)))))
+ ≡⟨
+ ∑∑Compat
+ (λ i j →
+ MF (toℕ (suc k) +ℕ toℕ i) · M (suc k) i ·
+ (MF (toℕ j) · minor (suc k) i M zero j ·
+ det (minor zero j (minor (suc k) i M))))
+ (λ i 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)))
+ (λ i j → DetRowAux1 (suc k) i j M)
+ ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ 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))))
+ ≡⟨ ∑∑Compat
+ (λ i 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)))
+ (λ i j →
+ 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)))
+ +
+ (1r + - 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))))
+ (λ i 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))))
+ ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ 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)))
+ +
+ (1r + - 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)))))
+ ≡⟨ ∑∑Split
+ (λ i j →
+ 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))))
+ (λ i j →
+ (1r + - 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))))
+ ⟩
+ (∑
+ (λ i →
+ ∑
+ (λ j →
+ 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)))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - 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))))))
+ ≡⟨ +Compat (DetRowAux3a k M) (DetRowAux3b k M) ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ (suc i)) (toℕ j) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ minor (suc k) (suc i) M zero j
+ · det (minor zero j (minor (suc k) (suc i) M)))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · minor (suc k) (weakenFin i) M zero j
+ · det (minor zero j (minor (suc k) (weakenFin i) M)))))
+ ≡⟨ +Compat (DetRowAux4a k M) (DetRowAux4b k M) ⟩
+ (∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M)))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (suc (toℕ j)) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M))))))
+ ≡⟨ +Compat (DetRowAux5a k M) (DetRowAux5b k M) ⟩
+ (∑
+ (λ j →
+ ∑
+ (λ i →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero (weakenFin j)
+ · det (minor k i (minor zero (weakenFin j) M))))) +
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ ind> (suc (toℕ j)) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (weakenFin i) +ℕ toℕ j) ·
+ M (suc k) (weakenFin i)
+ · M (weakenFin zero) (suc j)
+ · det (minor k i (minor zero (suc j) M))))))
+ ≡⟨ +Compat (DetRowAux6a k M) (DetRowAux6b k M) ⟩
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (suc i) ·
+ M zero j
+ · det (minor k i (minor zero j M)))))
+ +
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ ind> (toℕ j) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · M (suc k) (weakenFin i)
+ · M zero j
+ · det (minor k i (minor zero j M)))))
+ ≡⟨ +Compat (DetRowAux7a k M) (DetRowAux7b k M) ⟩
+ (∑
+ (λ j →
+ ∑
+ (λ i →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i ·
+ M zero j
+ · det (minor k i (minor zero j M)))))
+ +
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ ind> (toℕ j) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i ·
+ M zero j
+ · det (minor k i (minor zero j M))))))
+ ≡⟨ +Comm _ _ ⟩
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ ind> (toℕ j) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i ·
+ M zero j
+ · det (minor k i (minor zero j M)))))
+ +
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i ·
+ M zero j
+ · det (minor k i (minor zero j M)))))
+ ≡⟨ sym
+ (∑∑Split
+ (λ j i →
+ ind> (toℕ j) (toℕ i) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i ·
+ M zero j
+ · det (minor k i (minor zero j M))))
+ λ j i → (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc k) +ℕ toℕ (suc i) +ℕ toℕ j) · minor zero j M k i ·
+ M zero j
+ · det (minor k i (minor zero j M)))
+ ) ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ 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)))
+ +
+ (1r + - 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)))))
+ ≡⟨
+ ∑∑Compat
+ (λ i j →
+ (
+ 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)))
+ +
+ (1r + - 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)))))
+ (λ z z₁ →
+ MF (toℕ (suc k) +ℕ toℕ (suc z₁) +ℕ toℕ z) · minor zero z M k z₁ ·
+ M zero z
+ · det (minor k z₁ (minor zero z M)))
+ (λ i j →
+ sym
+ (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)))))
+ ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ 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))))
+ ≡⟨
+ ∑∑Compat
+ (λ i 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)))
+ (λ z z₁ →
+ MF (toℕ z) · M zero z ·
+ (MF (toℕ k +ℕ toℕ z₁) · minor zero z M k z₁ ·
+ det (minor k z₁ (minor zero z M))))
+ (λ i j → DetRowAux8 i j k M)
+ ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ MF (toℕ i) · M zero i · (MF (toℕ k +ℕ toℕ j) · minor zero i M k j
+ · det (minor k j (minor zero i M)))))
+ ≡⟨
+ ∑Compat
+ (λ i →
+ ∑
+ (λ j →
+ MF (toℕ i) · M zero i · (MF (toℕ k +ℕ toℕ j) · minor zero i M k j
+ · det (minor k j (minor zero i M)))))
+ (λ i →
+ MF (toℕ i) · M zero i ·
+ ∑
+ (λ j →
+ MF (toℕ k +ℕ toℕ j) · minor zero i M k j
+ · det (minor k j (minor zero i M))))
+ (λ i → sym
+ (∑DistR
+ ( MF (toℕ i) · M zero i)
+ (λ j → MF (toℕ k +ℕ toℕ j) · minor zero i M k j
+ · det (minor k j (minor zero i M)))))
+ ⟩
+ ∑
+ (λ i →
+ MF (toℕ i) · M zero i ·
+ ∑
+ (λ j →
+ MF (toℕ k +ℕ toℕ j) · minor zero i M k j
+ · det (minor k j (minor zero i M))))
+ ≡⟨ ∑Compat
+ (λ i →
+ MF (toℕ i) · M zero i ·
+ detR k (minor zero i M))
+ (λ i →
+ MF (toℕ i) · M zero i ·
+ det (minor zero i M))
+ (λ i →
+ cong
+ (λ a → MF (toℕ i) · M zero i · a)
+ (DetRow k (minor zero i M)))
+ ⟩
+ ∑ (λ i → MF (toℕ i) · M zero i · det (minor zero i M))
+ ∎
+
+ --Laplace expansion along columns
+
+ detC : ∀ {n} → (k : Fin n) → FinMatrix R n n → R
+ detC {suc n} k M = ∑ (λ i → (MF ((toℕ i) +ℕ (toℕ k))) · (M i k) · det {n} (minor i k M))
+
+ DetRowColumnAux : {n : ℕ} → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ MF (toℕ (suc i) +ℕ zero) · M (suc i) zero ·
+ (MF (toℕ j) · minor (suc i) zero M zero j ·
+ det (minor zero j (minor (suc i) zero M)))))
+ ≡
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ MF (toℕ (suc j))· M zero (suc j) ·
+ (MF (toℕ i +ℕ zero)· minor zero (suc j) M i zero ·
+ det (minor i zero (minor zero (suc j) M)))))
+
+ DetRowColumnAux M =
+ ∑∑Compat
+ (λ i j →
+ MF (toℕ (suc i) +ℕ zero) · M (suc i) zero ·
+ (MF (toℕ j) · minor (suc i) zero M zero j ·
+ det (minor zero j (minor (suc i) zero M))))
+ (λ i j →
+ MF (toℕ (suc j))· M zero (suc j) ·
+ (MF (toℕ i +ℕ zero)· minor zero (suc j) M i zero ·
+ det (minor i zero (minor zero (suc j) M))))
+ (λ i j →
+ (MF (toℕ (suc i) +ℕ zero) · M (suc i) zero ·
+ (MF (toℕ j) · minor (suc i) zero M zero j ·
+ det (minor zero j (minor (suc i) zero M))))
+ ≡⟨ cong
+ (λ a →
+ MF (toℕ (suc i) +ℕ zero) · M (suc i) zero ·
+ (MF (toℕ j) · a ·
+ det (minor zero j (minor (suc i) zero M))))
+ (minorIdSuc (suc i) zero zero j M (s≤s z≤) z≤)
+ ⟩
+ (MF (toℕ (suc i) +ℕ zero) · M (suc i) zero ·
+ (MF (toℕ j) · M zero (suc j) ·
+ det (minor zero j (minor (suc i) zero M))))
+ ≡⟨
+ cong
+ (λ a →
+ MF (toℕ (suc i) +ℕ zero) · M (suc i) zero ·
+ (MF (toℕ j) · M zero (suc j) · a))
+ (detComp
+ (minor zero j (minor (suc i) zero M))
+ (minor i zero (minor zero (suc j) M))
+ (λ i₁ j₁ → (minorComm1 i zero zero j i₁ j₁ M z≤ z≤)))
+ ⟩
+ (MF (toℕ (suc i) +ℕ zero) · M (suc i) zero ·
+ (MF (toℕ j) · M zero (suc j) ·
+ det (minor i zero (minor zero (suc j) M))))
+ ≡⟨ ·Assoc (MF (toℕ (suc i) +ℕ zero) · M (suc i) zero) (MF (toℕ j) · M zero (suc j)) (det (minor i zero (minor zero (suc j) M))) ⟩
+ MF (toℕ (suc i) +ℕ zero) · M (suc i) zero · (MF (toℕ j) · M zero (suc j)) ·
+ det (minor i zero (minor zero (suc j) M))
+ ≡⟨
+ cong
+ (λ a → a · M (suc i) zero ·
+ (MF (toℕ j) · M zero (suc j)) ·
+ det (minor i zero (minor zero (suc j) M)))
+ (MF (toℕ (suc i) +ℕ zero)
+ ≡⟨ sumMF (toℕ (suc i)) zero ⟩
+ (MF (toℕ (suc i)) · MF zero)
+ ≡⟨ solve! P' ⟩
+ MF (toℕ (suc i))
+ ∎)
+ ⟩
+ MF (toℕ (suc i)) · M (suc i) zero · (MF (toℕ j) · M zero (suc j)) ·
+ det (minor i zero (minor zero (suc j) M))
+ ≡⟨ cong
+ (λ a →
+ a ·
+ det (minor i zero (minor zero (suc j) M)))
+ (solve! P') ⟩
+ MF (toℕ (suc j)) · M zero (suc j) ·
+ MF (toℕ i) · M (suc i) zero ·
+ det (minor i zero (minor zero (suc j) M))
+ ≡⟨ sym (·Assoc (MF (toℕ (suc j)) · M zero (suc j) · MF (toℕ i)) (M (suc i) zero) (det (minor i zero (minor zero (suc j) M)))) ⟩
+ (MF (toℕ (suc j)) · M zero (suc j) · MF (toℕ i) ·
+ (M (suc i) zero · det (minor i zero (minor zero (suc j) M))))
+ ≡⟨ sym (·Assoc (MF (toℕ (suc j)) · M zero (suc j)) (MF (toℕ i)) (M (suc i) zero · det (minor i zero (minor zero (suc j) M)))) ⟩
+ (MF (toℕ (suc j)) · M zero (suc j) ·
+ (MF (toℕ i) ·
+ (M (suc i) zero · det (minor i zero (minor zero (suc j) M)))))
+ ≡⟨ cong (λ a → MF (toℕ (suc j)) · M zero (suc j) · a)
+ (·Assoc (MF (toℕ i)) (M (suc i) zero) (det (minor i zero (minor zero (suc j) M)))) ⟩
+ MF (toℕ (suc j)) · M zero (suc j) ·
+ (MF (toℕ i) · M (suc i) zero ·
+ det (minor i zero (minor zero (suc j) M)))
+ ≡⟨ refl ⟩
+ (MF (toℕ (suc j)) · M zero (suc j) ·
+ (MF (toℕ i) · minor zero (suc j) M i zero ·
+ det (minor i zero (minor zero (suc j) M))))
+ ≡⟨
+ cong
+ (λ a → (MF (toℕ (suc j)) · M zero (suc j) ·
+ (a · minor zero (suc j) M i zero ·
+ det (minor i zero (minor zero (suc j) M)))))
+ (MF (toℕ i)
+ ≡⟨ solve! P' ⟩
+ (MF (toℕ i) · MF zero)
+ ≡⟨ sym (sumMF (toℕ i) zero) ⟩
+ MF (toℕ i +ℕ zero) ∎)
+ ⟩
+ (MF (toℕ (suc j)) · M zero (suc j) ·
+ (MF (toℕ i +ℕ zero) · minor zero (suc j) M i zero ·
+ 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
+ DetRowColumn {suc n} M =
+ detC zero M
+ ≡⟨ refl ⟩
+ ∑ (λ i → (MF ((toℕ i) +ℕ zero)) · (M i zero) · det {suc n} (minor i zero M))
+ ≡⟨ refl ⟩
+ 1r · (M zero zero) · det (minor zero zero M) +
+ ∑ (λ i → (MF ((toℕ (suc i)) +ℕ zero)) · (M (suc i) zero) · det {suc n} (minor (suc i) zero M))
+ ≡⟨ refl ⟩
+ (1r · M zero zero · det (minor zero zero M) +
+ ∑ (λ i →
+ MF (toℕ (suc i) +ℕ zero) · M (suc i) zero ·
+ ∑ (λ j → MF (toℕ j) · minor (suc i) zero M zero j · det (minor zero j (minor (suc i) zero M)))))
+ ≡⟨ +Compat
+ refl
+ (∑Compat
+ (λ i → MF (toℕ (suc i) +ℕ zero) · M (suc i) zero ·
+ ∑ (λ j → MF (toℕ j) · minor (suc i) zero M zero j ·
+ det (minor zero j (minor (suc i) zero M))))
+ (λ i → ∑ (λ j → MF (toℕ (suc i) +ℕ zero) · M (suc i) zero ·
+ (MF (toℕ j) · minor (suc i) zero M zero j ·
+ det (minor zero j (minor (suc i) zero M)))))
+ (λ i → ∑DistR
+ (MF (toℕ (suc i) +ℕ zero) · M (suc i) zero)
+ (λ j → MF (toℕ j) · minor (suc i) zero M zero j · det (minor zero j (minor (suc i) zero M)))))
+ ⟩
+ 1r · M zero zero · det (minor zero zero M) +
+ ∑ (λ i →
+ ∑ (λ j →
+ MF (toℕ (suc i) +ℕ zero) · M (suc i) zero ·
+ (MF (toℕ j) · minor (suc i) zero M zero j ·
+ det (minor zero j (minor (suc i) zero M)))))
+ ≡⟨ +Compat refl (DetRowColumnAux M) ⟩
+ (1r · M zero zero · det (minor zero zero M) +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ MF (toℕ (suc j)) · M zero (suc j) ·
+ (MF (toℕ i +ℕ zero) · minor zero (suc j) M i zero ·
+ det (minor i zero (minor zero (suc j) M))))))
+ ≡⟨ +Compat refl (∑Comm
+ λ i j →
+ MF (toℕ (suc j)) · M zero (suc j) ·
+ (MF (toℕ i +ℕ zero) · minor zero (suc j) M i zero ·
+ det (minor i zero (minor zero (suc j) M)))) ⟩
+ (1r · M zero zero · det (minor zero zero M) +
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ MF (toℕ (suc j)) · M zero (suc j) ·
+ (MF (toℕ i +ℕ zero) · minor zero (suc j) M i zero ·
+ det (minor i zero (minor zero (suc j) M))))))
+ ≡⟨ +Compat
+ refl
+ (∑Compat (λ j →
+ ∑
+ (λ i →
+ MF (toℕ (suc j)) · M zero (suc j) ·
+ (MF (toℕ i +ℕ zero) · minor zero (suc j) M i zero ·
+ det (minor i zero (minor zero (suc j) M)))))
+ (λ j →
+ MF (toℕ (suc j)) · M zero (suc j) ·
+ ∑(λ i →
+ (MF (toℕ i +ℕ zero) · M (suc i) zero ·
+ det (minor i zero (minor zero (suc j) M)))))
+ (λ j → sym (∑DistR (MF (toℕ (suc j)) · M zero (suc j))
+ λ i → MF (toℕ i +ℕ zero) · M (suc i) zero ·
+ det (minor i zero (minor zero (suc j) M))) )) ⟩
+ (1r · M zero zero · det (minor zero zero M) +
+ ∑
+ (λ j →
+ MF (toℕ (suc j)) · M zero (suc j) ·
+ detC {suc n} zero (minor zero (suc j) M)))
+ ≡⟨ +Compat
+ refl
+ (∑Compat
+ (λ j →
+ MF (toℕ (suc j)) · M zero (suc j) ·
+ detC {suc n} zero (minor zero (suc j) M))
+ (λ j →
+ MF (toℕ (suc j)) · M zero (suc j) ·
+ det (minor zero (suc j) M))
+ (λ j → cong
+ (λ a → MF (toℕ (suc j)) · M zero (suc j) · a)
+ (DetRowColumn (minor zero (suc j) M))))
+ ⟩
+ (1r · M zero zero · det (minor zero zero M) +
+ ∑
+ (λ j →
+ MF (toℕ (suc j)) · M zero (suc j) ·
+ det (minor zero (suc j) M)))
+ ≡⟨ refl ⟩
+ det M
+ ∎
+
+ DetColumnAux1a : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ (suc i)) (toℕ j) ·
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero ·
+ det (minor j zero (minor (suc i) (suc k) M))))))
+ ≡
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ (weakenFin j)) (toℕ i)) ·
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ (weakenFin j) +ℕ zero) · M (weakenFin j) zero ·
+ det (minor i k (minor (weakenFin j) zero M))))))
+ DetColumnAux1a k M =
+ ∑∑Compat
+ (λ i j → ind> (toℕ (suc i)) (toℕ j) ·
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero ·
+ det (minor j zero (minor (suc i) (suc k) M)))))
+ (λ z z₁ →
+ (1r + - ind> (toℕ (weakenFin z₁)) (toℕ z)) ·
+ (MF (toℕ (suc z) +ℕ toℕ (suc k)) · M (suc z) (suc k) ·
+ (MF (toℕ (weakenFin z₁) +ℕ zero) · M (weakenFin z₁) zero ·
+ det (minor z k (minor (weakenFin z₁) zero M)))))
+ (λ i j →
+ (ind> (suc (toℕ i)) (toℕ j) ·
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero ·
+ det (minor j zero (minor (suc i) (suc k) M)))))
+ ≡⟨
+ cong
+ (λ a → a · (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero ·
+ det (minor j zero (minor (suc i) (suc k) M)))))
+ (ind>Suc (toℕ i) (toℕ j))
+ ⟩
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero ·
+ det (minor j zero (minor (suc i) (suc k) M))))
+ ≡⟨
+ ind>anti
+ (λ j i → (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero ·
+ det (minor j zero (minor (suc i) (suc k) M)))))
+ (λ z z₁ →
+ MF (toℕ (suc z₁) +ℕ toℕ (suc k)) · M (suc z₁) (suc k) ·
+ (MF (toℕ z +ℕ zero) · M (weakenFin z) zero ·
+ det (minor z₁ k (minor (weakenFin z) zero M))))
+ (λ j i le →
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero ·
+ det (minor j zero (minor (suc i) (suc k) M))))
+ ≡⟨ cong
+ (λ a → (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · a ·
+ det (minor j zero (minor (suc i) (suc k) M)))))
+ (minorIdId (suc i) (suc k) j zero M (s≤s le) (s≤s z≤))
+ ⟩
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · M (weakenFin j) zero ·
+ det (minor j zero (minor (suc i) (suc k) M))))
+ ≡⟨
+ cong
+ (λ a → (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · M (weakenFin j) zero · a)))
+ (detComp
+ (minor j zero (minor (suc i) (suc k) M))
+ (minor i k (minor (weakenFin j) zero M))
+ (λ i₁ j₁ →
+ minorComm0 i j k zero i₁ j₁ M le z≤))
+ ⟩
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · M (weakenFin j) zero ·
+ det (minor i k (minor (weakenFin j) zero M))))
+ ∎)
+ j
+ i ⟩
+ ((1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · M (weakenFin j) zero ·
+ det (minor i k (minor (weakenFin j) zero M)))))
+ ≡⟨
+ cong
+ (λ a →
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (a · M (weakenFin j) zero ·
+ det (minor i k (minor (weakenFin j) zero M)))))
+ (MF (toℕ j +ℕ zero)
+ ≡⟨ sumMF (toℕ j) zero ⟩
+ (MF (toℕ j) · MF zero)
+ ≡⟨ cong (λ a → MF a · MF zero) ((toℕ j) ≡⟨ sym (toℕweakenFin j) ⟩ toℕ (weakenFin j) ∎) ⟩
+ (MF (toℕ (weakenFin j)) · MF zero)
+ ≡⟨ sym (sumMF (toℕ (weakenFin j)) zero) ⟩
+ MF (toℕ (weakenFin j) +ℕ zero)
+ ∎)
+ ⟩
+ (1r + - ind> (toℕ j) (toℕ i)) ·
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ (weakenFin j) +ℕ zero) · M (weakenFin j) zero ·
+ det (minor i k (minor (weakenFin j) zero M))))
+ ≡⟨
+ cong
+ (λ a → (1r + - ind> a (toℕ i)) ·
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ (weakenFin j) +ℕ zero) · M (weakenFin j) zero ·
+ det (minor i k (minor (weakenFin j) zero M)))))
+ (toℕ j ≡⟨ sym (toℕweakenFin j) ⟩ toℕ (weakenFin j) ∎)
+ ⟩
+ ((1r + - ind> (toℕ (weakenFin j)) (toℕ i)) ·
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ (weakenFin j) +ℕ zero) · M (weakenFin j) zero ·
+ det (minor i k (minor (weakenFin j) zero M)))))
+ ∎)
+
+
+ DetColumnAux1b : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) ·
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero ·
+ det (minor j zero (minor (weakenFin i) (suc k) M))))))
+ ≡
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (toℕ (suc z)) (toℕ i) ·
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ (suc z) +ℕ one) · M (suc z) zero ·
+ det (minor i k (minor (suc z) zero M))))))
+ DetColumnAux1b k M =
+ ∑∑Compat
+ (λ i j →
+ (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) ·
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero ·
+ det (minor j zero (minor (weakenFin i) (suc k) M)))))
+ (λ z z₁ →
+ ind> (toℕ (suc z₁)) (toℕ z) ·
+ (MF (toℕ (weakenFin z) +ℕ toℕ (suc k)) · M (weakenFin z) (suc k) ·
+ (MF (toℕ (suc z₁) +ℕ one) · M (suc z₁) zero ·
+ det (minor z k (minor (suc z₁) zero M)))))
+ (λ i j →
+ ((1r + - ind> (toℕ (weakenFin i)) (toℕ j)) ·
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero ·
+ det (minor j zero (minor (weakenFin i) (suc k) M)))))
+ ≡⟨ cong
+ (λ a → (1r + - ind> a (toℕ j)) ·
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero ·
+ det (minor j zero (minor (weakenFin i) (suc k) M)))))
+ (toℕweakenFin i) ⟩
+ ((1r + - ind> (toℕ i) (toℕ j)) ·
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero ·
+ det (minor j zero (minor (weakenFin i) (suc k) M)))))
+ ≡⟨ ind>anti
+ (λ i j → MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero ·
+ det (minor j zero (minor (weakenFin i) (suc k) M))))
+ (λ i j → MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · M (suc j) zero ·
+ det (minor i k (minor (suc j) zero M))))
+ (λ i j le →
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero ·
+ det (minor j zero (minor (weakenFin i) (suc k) M))))
+ ≡⟨ cong
+ (λ a →
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · a ·
+ det (minor j zero (minor (weakenFin i) (suc k) M)))))
+ (minorSucId
+ (weakenFin i)
+ (suc k)
+ j
+ zero
+ M
+ (weakenweakenFinLe i j le)
+ (s≤s z≤))
+ ⟩
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · M (suc j) zero ·
+ det (minor j zero (minor (weakenFin i) (suc k) M))))
+ ≡⟨
+ cong
+ (λ a →
+ MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · M (suc j) zero · a))
+ (detComp
+ (minor j zero (minor (weakenFin i) (suc k) M))
+ (minor i k (minor (suc j) zero M))
+ λ i₁ j₁ →
+ minorComm2
+ i
+ j
+ k
+ zero
+ i₁
+ j₁
+ M
+ le
+ z≤)
+ ⟩
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · M (suc j) zero ·
+ det (minor i k (minor (suc j) zero M))))
+ ∎)
+ i
+ j
+ ⟩
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · M (suc j) zero ·
+ det (minor i k (minor (suc j) zero M))))
+ ≡⟨ cong
+ (λ a → a · (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · M (suc j) zero ·
+ det (minor i k (minor (suc j) zero M)))))
+ (sym (ind>Suc (toℕ j) (toℕ i))) ⟩
+ (ind> (toℕ (suc j)) (toℕ i) ·
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · M (suc j) zero ·
+ det (minor i k (minor (suc j) zero M)))))
+ ≡⟨
+ cong
+ (λ a → (ind> (toℕ (suc j)) (toℕ i) ·
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (a · M (suc j) zero ·
+ det (minor i k (minor (suc j) zero M))))))
+ (MF (toℕ j +ℕ zero)
+ ≡⟨ sumMF (toℕ j) zero ⟩
+ (MF (toℕ j) · MF zero)
+ ≡⟨ solve! P' ⟩
+ (MF (toℕ (suc j)) · MF one)
+ ≡⟨ sym (sumMF (toℕ (suc j)) one) ⟩
+ MF (toℕ (suc j) +ℕ one)
+ ∎)
+ ⟩
+ (ind> (toℕ (suc j)) (toℕ i) ·
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ (suc j) +ℕ one) · M (suc j) zero ·
+ det (minor i k (minor (suc j) zero M)))))
+ ∎)
+
+ DetColumnAux2a : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (MF (toℕ (suc j) +ℕ toℕ (suc k)) · M (suc j) (suc k) ·
+ (MF (toℕ i +ℕ zero) · M i zero ·
+ det (minor j k (minor i zero M))))))
+ ≡
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - 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))))))
+
+ DetColumnAux2a k M =
+ ∑∑Compat
+ (λ i j →
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (MF (toℕ (suc j) +ℕ toℕ (suc k)) · M (suc j) (suc k) ·
+ (MF (toℕ i +ℕ zero) · M i zero ·
+ det (minor j k (minor i zero M)))))
+ (λ z z₁ →
+ (1r + - ind> (toℕ z) (toℕ z₁)) ·
+ (MF (toℕ z +ℕ zero) · M z zero ·
+ (MF (toℕ (suc z₁) +ℕ toℕ (suc k)) · minor z zero M z₁ k ·
+ det (minor z₁ k (minor z zero M)))))
+ (ind>anti
+ (λ i j →
+ MF (toℕ (suc j) +ℕ toℕ (suc k)) · M (suc j) (suc k) ·
+ (MF (toℕ i +ℕ zero) · M i zero · det (minor j k (minor i zero M))))
+ (λ z z₁ →
+ MF (toℕ z +ℕ zero) · M z zero ·
+ (MF (toℕ (suc z₁) +ℕ toℕ (suc k)) · minor z zero M z₁ k ·
+ det (minor z₁ k (minor z zero M))))
+ (λ i j le →
+ (MF (toℕ (suc j) +ℕ toℕ (suc k)) · M (suc j) (suc k) ·
+ (MF (toℕ i +ℕ zero) · M i zero · det (minor j k (minor i zero M))))
+ ≡⟨ cong
+ (λ a →
+ (MF (toℕ (suc j) +ℕ toℕ (suc k)) · a ·
+ (MF (toℕ i +ℕ zero) · M i zero · det (minor j k (minor i zero M)))))
+ (sym
+ (minorSucSuc i zero j k M (weakenFinLe i j le) z≤))
+ ⟩
+ (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k ·
+ (MF (toℕ i +ℕ zero) · M i zero · det (minor j k (minor i zero M))))
+ ≡⟨
+ cong
+ (λ a → (a · minor i zero M j k ·
+ (MF (toℕ i +ℕ zero) · M i zero · det (minor j k (minor i zero M)))))
+ (sumMF (toℕ (suc j)) (toℕ (suc k)))
+ ⟩
+ (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ (MF (toℕ i +ℕ zero) · M i zero · det (minor j k (minor i zero M))))
+ ≡⟨
+ cong
+ (λ a → (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ (a · M i zero · det (minor j k (minor i zero M)))))
+ (sumMF (toℕ i) zero)
+ ⟩
+ (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ (MF (toℕ i) · MF zero · M i zero ·
+ det (minor j k (minor i zero M))))
+ ≡⟨ ·Assoc
+ (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k)
+ (MF (toℕ i) · MF zero · M i zero)
+ (det (minor j k (minor i zero M))) ⟩
+ (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ (MF (toℕ i) · MF zero · M i zero)
+ · det (minor j k (minor i zero M)))
+ ≡⟨
+ cong
+ (λ a → a
+ · det (minor j k (minor i zero M)))
+ (solve! P')
+ ⟩
+ (MF (toℕ i) · MF zero · M i zero) ·
+ (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k)
+ · det (minor j k (minor i zero M))
+ ≡⟨
+ sym
+ (·Assoc
+ (MF (toℕ i) · MF zero · M i zero)
+ (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k)
+ (det (minor j k (minor i zero M))))
+ ⟩
+ MF (toℕ i) · MF zero · M i zero ·
+ (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ det (minor j k (minor i zero M)))
+ ≡⟨
+ cong
+ (λ a → (a · M i zero ·
+ (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ det (minor j k (minor i zero M)))))
+ (sym (sumMF (toℕ i) zero))
+ ⟩
+ (MF (toℕ i +ℕ zero) · M i zero ·
+ (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ det (minor j k (minor i zero M))))
+ ≡⟨
+ cong
+ (λ a → (MF (toℕ i +ℕ zero) · M i zero ·
+ (a · minor i zero M j k · det (minor j k (minor i zero M)))))
+ (sym (sumMF (toℕ (suc j)) (toℕ (suc k))))
+ ⟩
+ (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))))
+
+ ∎)
+ )
+
+ DetColumnAux2b : {n : ℕ} → (k : Fin (suc n)) → (M : FinMatrix R (suc (suc n)) (suc (suc n))) →
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ i) (toℕ j) ·
+ (MF (toℕ (weakenFin j) +ℕ toℕ (suc k)) · M (weakenFin j) (suc k) ·
+ (MF (toℕ i +ℕ one) · M i zero ·
+ det (minor j k (minor i zero M))))))
+ ≡
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ 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))))))
+ DetColumnAux2b k M =
+ ∑∑Compat
+ (λ i j → ind> (toℕ i) (toℕ j) ·
+ (MF (toℕ (weakenFin j) +ℕ toℕ (suc k)) · M (weakenFin j) (suc k) ·
+ (MF (toℕ i +ℕ one) · M i zero ·
+ det (minor j k (minor i zero M)))))
+ (λ z z₁ →
+ ind> (toℕ z) (toℕ z₁) ·
+ (MF (toℕ z +ℕ zero) · M z zero ·
+ (MF (toℕ (suc z₁) +ℕ toℕ (suc k)) · minor z zero M z₁ k ·
+ det (minor z₁ k (minor z zero M)))))
+ (λ i j →
+ ind>prop
+ (λ i j → (MF (toℕ (weakenFin j) +ℕ toℕ (suc k)) · M (weakenFin j) (suc k) ·
+ (MF (toℕ i +ℕ one) · M i zero ·
+ det (minor j k (minor i zero M)))))
+ (λ z z₁ →
+ MF (toℕ z +ℕ zero) · M z zero ·
+ (MF (toℕ (suc z₁) +ℕ toℕ (suc k)) · minor z zero M z₁ k ·
+ det (minor z₁ k (minor z zero M))))
+ (λ i j le →
+ (MF (toℕ (weakenFin j) +ℕ toℕ (suc k)) · M (weakenFin j) (suc k) ·
+ (MF (toℕ i +ℕ one) · M i zero · det (minor j k (minor i zero M))))
+ ≡⟨
+ cong
+ (λ a →
+ (MF (toℕ (weakenFin j) +ℕ toℕ (suc k)) · a ·
+ (MF (toℕ i +ℕ one) · M i zero · det (minor j k (minor i zero M)))))
+ (sym (minorIdSuc i zero j k M le z≤))
+ ⟩
+ (MF (toℕ (weakenFin j) +ℕ toℕ (suc k)) · minor i zero M j k ·
+ (MF (toℕ i +ℕ one) · M i zero · det (minor j k (minor i zero M))))
+ ≡⟨
+ cong
+ (λ a → a · minor i zero M j k ·
+ (MF (toℕ i +ℕ one) · M i zero · det (minor j k (minor i zero M))))
+ (sumMF (toℕ (weakenFin j)) (toℕ (suc k)))
+ ⟩
+ (MF (toℕ (weakenFin j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ (MF (toℕ i +ℕ one) · M i zero · det (minor j k (minor i zero M))))
+ ≡⟨
+ cong
+ (λ a → MF (toℕ (weakenFin j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ (a · M i zero · det (minor j k (minor i zero M))))
+ (sumMF (toℕ i) one)
+ ⟩
+ (MF (toℕ (weakenFin j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ (MF (toℕ i) · MF one · M i zero · det (minor j k (minor i zero M))))
+ ≡⟨ cong
+ (λ a → (MF (a) · MF (toℕ (suc k)) · minor i zero M j k ·
+ (MF (toℕ i) · MF one · M i zero · det (minor j k (minor i zero M)))))
+ (toℕweakenFin j) ⟩
+ (MF (toℕ j) · MF (toℕ (suc k)) · minor i zero M j k ·
+ (MF (toℕ i) · MF one · M i zero · det (minor j k (minor i zero M))))
+ ≡⟨ ·Assoc
+ (MF (toℕ j) · MF (toℕ (suc k)) · minor i zero M j k)
+ (MF (toℕ i) · MF one · M i zero)
+ (det (minor j k (minor i zero M))) ⟩
+ (MF (toℕ j) · MF (toℕ (suc k)) · minor i zero M j k ·
+ (MF (toℕ i) · MF one · M i zero)
+ · det (minor j k (minor i zero M)))
+ ≡⟨ cong
+ (λ a → a · det (minor j k (minor i zero M)))
+ (solve! P') ⟩
+ (MF one · MF (toℕ j) · MF (toℕ (suc k)) · minor i zero M j k ·
+ (MF (toℕ i) · M i zero)
+ · det (minor j k (minor i zero M)))
+ ≡⟨
+ cong
+ (λ a → a · MF (toℕ (suc k)) · minor i zero M j k ·
+ (MF (toℕ i) · M i zero)
+ · det (minor j k (minor i zero M)))
+ (sym (sumMF one (toℕ j)))
+ ⟩
+ (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ (MF (toℕ i) · M i zero)
+ · det (minor j k (minor i zero M)))
+ ≡⟨
+ cong
+ (λ a → a · det (minor j k (minor i zero M)))
+ (solve! P')
+ ⟩
+ (MF (toℕ i) · M i zero)
+ · MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ det (minor j k (minor i zero M))
+ ≡⟨
+ cong
+ (λ a → ( a · M i zero)
+ · MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ det (minor j k (minor i zero M)))
+ (solve! P') ⟩
+ (MF (toℕ i) · MF zero · M i zero)
+ · MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ det (minor j k (minor i zero M))
+ ≡⟨
+ cong
+ (λ a → a · det (minor j k (minor i zero M)))
+ (solve! P')
+ ⟩
+ MF (toℕ i) · MF zero · M i zero ·
+ (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k)
+ · det (minor j k (minor i zero M))
+ ≡⟨ sym
+ (·Assoc
+ (MF (toℕ i) · MF zero · M i zero)
+ (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k)
+ (det (minor j k (minor i zero M)))) ⟩
+ MF (toℕ i) · MF zero · M i zero ·
+ (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ det (minor j k (minor i zero M)))
+ ≡⟨
+ cong
+ (λ a → (a · M i zero ·
+ (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ det (minor j k (minor i zero M)))))
+ (sym (sumMF (toℕ i) zero))
+ ⟩
+ (MF (toℕ i +ℕ zero) · M i zero ·
+ (MF (toℕ (suc j)) · MF (toℕ (suc k)) · minor i zero M j k ·
+ det (minor j k (minor i zero M))))
+ ≡⟨
+ cong
+ (λ a → (MF (toℕ i +ℕ zero) · M i zero ·
+ (a · minor i zero M j k · det (minor j k (minor i zero M)))))
+ (sym (sumMF (toℕ (suc j)) (toℕ (suc k))))
+ ⟩
+ (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))))
+ ∎)
+ i
+ j)
+
+ -- 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
+ DetColumnZero {suc n} zero M = refl
+ DetColumnZero {suc n} (suc k) M =
+ detC (suc k) M
+ ≡⟨ refl ⟩
+ ∑
+ (λ i →
+ MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · det (minor i (suc k) M))
+ ≡⟨ ∑Compat
+ (λ i →
+ MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · det (minor i (suc k) M))
+ (λ i →
+ MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · detC zero (minor i (suc k) M))
+ (λ i → cong
+ (λ a → MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · a)
+ (sym (DetRowColumn (minor i (suc k) M))))
+ ⟩
+ ∑
+ (λ i →
+ MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) · detC zero (minor i (suc k) M))
+ ≡⟨ refl ⟩
+ ∑
+ (λ i →
+ MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) ·
+ ∑
+ (λ j →
+ MF (toℕ j +ℕ zero) · minor i (suc k) M j zero ·
+ det (minor j zero (minor i (suc k) M))))
+ ≡⟨ ∑Compat
+ ((λ i →
+ MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) ·
+ ∑
+ (λ j →
+ MF (toℕ j +ℕ zero) · minor i (suc k) M j zero ·
+ det (minor j zero (minor i (suc k) M)))))
+ (λ i → ∑
+ (λ j →
+ MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero ·
+ det (minor j zero (minor i (suc k) M)))))
+ (λ i →
+ ∑DistR ( MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k))
+ (λ j →
+ (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero ·
+ det (minor j zero (minor i (suc k) M)))))
+ ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero ·
+ det (minor j zero (minor i (suc k) M)))))
+ ≡⟨
+ ∑∑Compat
+ (λ i j →
+ MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero ·
+ det (minor j zero (minor i (suc k) M))))
+ (λ z z₁ →
+ ind> (toℕ z) (toℕ z₁) ·
+ (MF (toℕ z +ℕ toℕ (suc k)) · M z (suc k) ·
+ (MF (toℕ z₁ +ℕ zero) · minor z (suc k) M z₁ zero ·
+ det (minor z₁ zero (minor z (suc k) M))))
+ +
+ (1r + - ind> (toℕ z) (toℕ z₁)) ·
+ (MF (toℕ z +ℕ toℕ (suc k)) · M z (suc k) ·
+ (MF (toℕ z₁ +ℕ zero) · minor z (suc k) M z₁ zero ·
+ det (minor z₁ zero (minor z (suc k) M)))))
+ (λ i j →
+ 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 ·
+ det (minor j zero (minor i (suc k) M)))))
+ ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ 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 ·
+ det (minor j zero (minor i (suc k) M))))
+ +
+ (1r + - 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 ·
+ det (minor j zero (minor i (suc k) M))))))
+ ≡⟨ ∑∑Split
+ (λ i j →
+ 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 ·
+ det (minor j zero (minor i (suc k) M)))))
+ (λ i j →
+ (1r + - 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 ·
+ det (minor j zero (minor i (suc k) M)))))
+ ⟩
+ (∑
+ (λ i →
+ ∑
+ (λ j →
+ 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 ·
+ det (minor j zero (minor i (suc k) M))))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - 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 ·
+ det (minor j zero (minor i (suc k) M)))))))
+ ≡⟨
+ +Compat
+ (∑∑ShiftSuc (λ i j →
+ MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero ·
+ det (minor j zero (minor i (suc k) M)))))
+ (∑∑ShiftWeak (λ i j → MF (toℕ i +ℕ toℕ (suc k)) · M i (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor i (suc k) M j zero ·
+ det (minor j zero (minor i (suc k) M)))))
+ ⟩
+ (∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ (suc i)) (toℕ j) ·
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (suc i) (suc k) M j zero ·
+ det (minor j zero (minor (suc i) (suc k) M))))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) ·
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · minor (weakenFin i) (suc k) M j zero ·
+ det (minor j zero (minor (weakenFin i) (suc k) M)))))))
+ ≡⟨ +Compat (DetColumnAux1a k M) (DetColumnAux1b k M) ⟩
+ (
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ (weakenFin j)) (toℕ i)) ·
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ (weakenFin j) +ℕ zero) · M (weakenFin j) zero ·
+ det (minor i k (minor (weakenFin j) zero M))))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ z →
+ ind> (toℕ (suc z)) (toℕ i) ·
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ (suc z) +ℕ one) · M (suc z) zero ·
+ det (minor i k (minor (suc z) zero M)))))))
+ ≡⟨ +Compat
+ (∑Comm (λ i j →
+ (1r + - ind> (toℕ (weakenFin j)) (toℕ i)) ·
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ (weakenFin j) +ℕ zero) · M (weakenFin j) zero ·
+ det (minor i k (minor (weakenFin j) zero M))))))
+ (∑Comm (λ i j →
+ ind> (toℕ (suc j)) (toℕ i) ·
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ (suc j) +ℕ one) · M (suc j) zero ·
+ det (minor i k (minor (suc j) zero M))))))
+ ⟩
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ (1r + - ind> (toℕ (weakenFin j)) (toℕ i)) ·
+ (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ (weakenFin j) +ℕ zero) · M (weakenFin j) zero ·
+ det (minor i k (minor (weakenFin j) zero M))))))
+ +
+ ∑
+ (λ j →
+ ∑
+ (λ i →
+ ind> (toℕ (suc j)) (toℕ i) ·
+ (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ (suc j) +ℕ one) · M (suc j) zero ·
+ det (minor i k (minor (suc j) zero M))))))
+ ≡⟨ +Compat
+ (sym (∑∑ShiftWeak (λ j i → (MF (toℕ (suc i) +ℕ toℕ (suc k)) · M (suc i) (suc k) ·
+ (MF (toℕ j +ℕ zero) · M j zero ·
+ det (minor i k (minor j zero M)))))))
+ (sym (∑∑ShiftSuc (λ j i → (MF (toℕ (weakenFin i) +ℕ toℕ (suc k)) · M (weakenFin i) (suc k) ·
+ (MF (toℕ j +ℕ one) · M j zero ·
+ det (minor i k (minor j zero M)))))))
+ ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ i) (toℕ j)) ·
+ (MF (toℕ (suc j) +ℕ toℕ (suc k)) · M (suc j) (suc k) ·
+ (MF (toℕ i +ℕ zero) · M i zero ·
+ det (minor j k (minor i zero M))))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ ind> (toℕ i) (toℕ j) ·
+ (MF (toℕ (weakenFin j) +ℕ toℕ (suc k)) · M (weakenFin j) (suc k) ·
+ (MF (toℕ i +ℕ one) · M i zero ·
+ det (minor j k (minor i zero M))))))
+ ≡⟨ +Compat (DetColumnAux2a k M) (DetColumnAux2b k M) ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - 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))))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ 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))))))
+ ≡⟨ +Comm ( ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - 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))))))) (∑
+ (λ i →
+ ∑
+ (λ j →
+ 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))))))) ⟩
+ (∑
+ (λ i →
+ ∑
+ (λ j →
+ 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))))))
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - 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)))))))
+ ≡⟨ sym (∑∑Split
+ (λ i j →
+ 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)))))
+ (λ i j →
+ (1r + - 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))))))
+ ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ 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))))
+ +
+ (1r + - 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))))))
+ ≡⟨ ∑∑Compat
+ (λ i j →
+ 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))))
+ +
+ (1r + - 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)))))
+ (λ i 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)))))
+ (λ i j → sym
+ (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))))))) ⟩
+ ∑
+ (λ i →
+ ∑
+ (λ 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)))))
+ ≡⟨ ∑Compat
+ ((λ i →
+ ∑
+ (λ 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))))))
+ ((λ i →
+ MF (toℕ i +ℕ zero) · M i zero ·
+ ∑
+ (λ j →
+ (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k ·
+ det (minor j k (minor i zero M))))))
+ (λ i →
+ sym
+ (∑DistR
+ (MF (toℕ i +ℕ zero) · M i zero)
+ (λ j →
+ (MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k ·
+ det (minor j k (minor i zero M))))))
+ ⟩
+ ∑
+ (λ i →
+ MF (toℕ i +ℕ zero) · M i zero ·
+ ∑
+ (λ j →
+ MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k ·
+ det (minor j k (minor i zero M))))
+ ≡⟨ ∑Compat
+ (λ i →
+ MF (toℕ i +ℕ zero) · M i zero ·
+ ∑
+ (λ j →
+ MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k ·
+ det (minor j k (minor i zero M))))
+ (λ i →
+ MF (toℕ i +ℕ zero) · M i zero ·
+ ∑
+ (λ j →
+ MF (toℕ j +ℕ toℕ k) · minor i zero M j k ·
+ det (minor j k (minor i zero M))))
+ (λ i →
+ cong
+ (λ a → MF (toℕ i +ℕ zero) · M i zero · a)
+ (∑Compat
+ (λ j →
+ MF (toℕ (suc j) +ℕ toℕ (suc k)) · minor i zero M j k ·
+ det (minor j k (minor i zero M)))
+ (λ j →
+ MF (toℕ j +ℕ toℕ k) · minor i zero M j k ·
+ det (minor j k (minor i zero M)))
+ (λ j →
+ cong
+ (λ a → a · minor i zero M j k ·
+ det (minor j k (minor i zero M)))
+ (MFsucsuc j k) )
+ ))⟩
+ ∑
+ (λ i →
+ MF (toℕ i +ℕ zero) · M i zero ·
+ ∑
+ (λ j →
+ MF (toℕ j +ℕ toℕ k) · minor i zero M j k ·
+ det (minor j k (minor i zero M))))
+ ≡⟨ refl ⟩
+ ∑
+ (λ i →
+ MF (toℕ i +ℕ zero) · M i zero ·
+ detC k (minor i zero M))
+ ≡⟨ ∑Compat
+ (λ i → MF (toℕ i +ℕ zero) · M i zero ·
+ detC k (minor i zero M))
+ (λ i → MF (toℕ i +ℕ zero) · M i zero ·
+ detC zero (minor i zero M))
+ (λ i → cong
+ (λ a → MF (toℕ i +ℕ zero) · M i zero · a)
+ (DetColumnZero k (minor i zero M))) ⟩
+ ∑
+ (λ i → MF (toℕ i +ℕ zero) · M i zero · detC zero (minor i zero M))
+ ≡⟨ ∑Compat
+ (λ i → MF (toℕ i +ℕ zero) · M i zero ·
+ detC zero (minor i zero M))
+ (λ i → MF (toℕ i +ℕ zero) · M i zero ·
+ det (minor i zero M))
+ (λ i → cong
+ (λ a → MF (toℕ i +ℕ zero) · M i zero · a)
+ (DetRowColumn (minor i zero M))) ⟩
+ ∑ (λ i → MF (toℕ i +ℕ zero) · M i zero · det (minor i zero M))
+ ≡⟨ refl ⟩
+ 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 =
+ detC k M
+ ≡⟨ DetColumnZero k M ⟩
+ detC zero M
+ ≡⟨ DetRowColumn M ⟩
+ det M
+ ∎
+
+ open Coefficient (P')
+
+ δ = KroneckerDelta.δ R'
+
+ ∑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
+ (λ i → MF (toℕ i) · 0r · det {n} (minor zero i 𝟘))
+ (λ i →
+ (MF (toℕ i) · 0r · det {n} (minor zero i 𝟘))
+ ≡⟨
+ cong
+ (λ a → a · det {n} (minor zero i 𝟘))
+ (solve! P')⟩
+ 0r · det (minor zero i 𝟘)
+ ≡⟨ RingTheory.0LeftAnnihilates (CommRing→Ring P') (det (minor zero i 𝟘)) ⟩
+ 0r
+ ∎
+ )
+
+ --The determinant of the identity matrix is 1.
+ detOne : {n : ℕ} → det {n} 𝟙 ≡ 1r
+ detOne {zero} = refl
+ detOne {suc n} =
+ ∑ (λ i → MF (toℕ i) · 𝟙 (zero {n}) i · det {n} (minor zero i 𝟙))
+ ≡⟨ refl ⟩
+ ∑ (λ i → MF (toℕ i) · δ (zero {n}) i · det {n} (minor zero i 𝟙))
+ ≡⟨ ∑Compat
+ (λ i → MF (toℕ i) · δ (zero {n}) i · det {n} (minor zero i 𝟙))
+ (λ i → δ (zero {n}) i · MF (toℕ i) · det {n} (minor zero i 𝟙))
+ (λ i →
+ cong
+ (λ a → a · det {n} (minor zero i 𝟙))
+ (solve! P'))
+ ⟩
+ ∑ (λ i → δ (zero {n}) i · MF (toℕ i) · det (minor zero i 𝟙))
+ ≡⟨ ∑Compat
+ (λ i → δ (zero {n}) i · MF (toℕ i) · det (minor zero i 𝟙))
+ (λ i → δ (zero {n}) i · (MF (toℕ i) · det (minor zero i 𝟙)))
+ (λ i → sym (·Assoc _ _ _)) ⟩
+ ∑ (λ i → δ (zero {n}) i · (MF (toℕ i) · det (minor zero i 𝟙)))
+ ≡⟨ ∑Mul1r
+ (suc n)
+ (λ i → (MF (toℕ i) · det {n} (minor zero i 𝟙)))
+ zero ⟩
+ MF zero · det {n} (minor zero zero 𝟙)
+ ≡⟨ refl ⟩
+ (1r · det {n} 𝟙)
+ ≡⟨ ·IdL (det {n} 𝟙) ⟩
+ det {n} 𝟙
+ ≡⟨ detOne{n} ⟩
+ 1r
+ ∎
+
+ --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 =
+ det M
+ ≡⟨ refl ⟩
+ ∑ (λ i → MF (toℕ i) · (M ᵗ) i zero · det ((minor i zero (M ᵗ))ᵗ))
+ ≡⟨
+ ∑Compat
+ (λ i → MF (toℕ i) · (M ᵗ) i zero · det ((minor i zero (M ᵗ))ᵗ))
+ (λ i → MF (toℕ i) · (M ᵗ) i zero · det (minor i zero (M ᵗ)))
+ (λ i →
+ cong
+ (λ a → MF (toℕ i) · (M ᵗ) i zero · a)
+ (sym (detTransp (minor i zero (M ᵗ)))))
+ ⟩
+ ∑ (λ i → MF (toℕ i) · (M ᵗ) i zero · det (minor i zero (M ᵗ)))
+ ≡⟨ ∑Compat
+ (λ i → MF (toℕ i) · (M ᵗ) i zero · det (minor i zero (M ᵗ)))
+ (λ i → MF (toℕ i +ℕ zero) · (M ᵗ) i zero · det (minor i zero (M ᵗ)))
+ (λ i →
+ cong
+ (λ a →
+ a · (M ᵗ) i zero · det (minor i zero (M ᵗ)))
+ (sym (MFplusZero i))) ⟩
+ ∑ (λ i → MF (toℕ i +ℕ zero) · (M ᵗ) i zero · det (minor i zero (M ᵗ)))
+ ≡⟨ (DetRowColumn ((M ᵗ))) ⟩
+ det (M ᵗ)
+ ∎
diff --git a/Cubical/Algebra/Determinat/Minor.agda b/Cubical/Algebra/Determinat/Minor.agda
new file mode 100644
index 000000000..50af7d503
--- /dev/null
+++ b/Cubical/Algebra/Determinat/Minor.agda
@@ -0,0 +1,195 @@
+{-# OPTIONS --cubical #-}
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.Determinat.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))
+ ∎
+
+ minorSemiCommR : {A : Type ℓ} {n m : ℕ} (i₁ : Fin (suc (suc n))) (i₂ : Fin (suc n)) (j₁ j₂ : Fin (suc m)) (k : Fin n) (l : Fin m) (M : FinMatrix A (suc (suc n)) (suc (suc m))) →
+ j₂ ≤'Fin j₁ →
+ minor i₂ j₂ (minor i₁ (suc j₁) M) k l ≡ minor i₂ j₁ (minor i₁ (weakenFin j₂) M) k l
+ minorSemiCommR i₁ i₂ j₁ j₂ k l M lej =
+ cong
+ (λ a → M (removeIndex i₁ (removeIndex i₂ k)) a)
+ (removeIndexComm j₂ j₁ l lej)
+
+
+ --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)
+ ∎
+
diff --git a/Cubical/Algebra/Determinat/RingSum.agda b/Cubical/Algebra/Determinat/RingSum.agda
new file mode 100644
index 000000000..aeeba7fb0
--- /dev/null
+++ b/Cubical/Algebra/Determinat/RingSum.agda
@@ -0,0 +1,349 @@
+{-# OPTIONS --cubical #-}
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.Determinat.RingSum where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+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.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 RingSum (ℓ : Level) (P' : CommRing ℓ) where
+
+ R' = CommRing→Ring P'
+
+ open RingStr (snd (CommRing→Ring P')) renaming ( is-set to isSetR)
+
+ ∑ = Sum.∑ (CommRing→Ring P')
+
+ R : Type ℓ
+ R = ⟨ P' ⟩
+
+ open MonoidBigOp (Ring→AddMonoid R')
+
+
+
+ -- Compatability theorems
+ ∑Compat : {n : ℕ} → (U V : FinVec R n) →
+ ((i : Fin n) → U i ≡ V i) → ∑ U ≡ ∑ V
+ ∑Compat U V f = bigOpExt f
+
+ ∑∑Compat : {n m : ℕ} → (U V : FinVec (FinVec R m) n) →
+ ((i : Fin n) → (j : Fin m) → U i j ≡ V i j) →
+ ∑ (λ i → ∑ (λ j → U i j)) ≡ ∑ (λ i → ∑ (λ j → V i j))
+ ∑∑Compat U V Eq =
+ ∑ (λ i → ∑ (U i))
+ ≡⟨
+ ∑Compat
+ (λ i → ∑ (U i))
+ (λ i → ∑ (V i))
+ (λ i → ∑Compat (U i) (V i) (Eq i))
+ ⟩
+ ∑ (λ i → ∑ (V i))
+ ∎
+
+ -- Spliting a sum in the sum:
+ ∑Split = Sum.∑Split R'
+
+ ∑∑Split : {n m : ℕ} → (U V : Fin n → Fin m → R) →
+ ∑ (λ i → ∑ (λ j → U i j + V i j))
+ ≡
+ ∑ (λ i → ∑ (λ j → U i j)) +
+ ∑ (λ i → ∑ (λ j → V i j))
+ ∑∑Split U V =
+ ∑ (λ i → ∑ (λ j → U i j + V i j))
+ ≡⟨
+ ∑Compat
+ (λ i → ∑ (λ j → U i j + V i j))
+ (λ i → ∑ (λ j → U i j) + ∑ ( λ j → V i j))
+ (λ i → ∑Split (λ j → U i j) ( λ j → V i j))
+ ⟩
+ ∑ (λ i → ∑ (λ j → U i j) + ∑ (λ j → V i j))
+ ≡⟨ ∑Split (λ i → ∑ (λ j → U i j)) (λ i → ∑ (λ j → V i j)) ⟩
+ (∑ (λ i → ∑ (U i)) + ∑ (λ i → ∑ (V i)))
+ ∎
+
+ -- Distributivity of the sum
+ ∑DistR = Sum.∑Mulrdist (CommRing→Ring P')
+
+ ∑DistL = Sum.∑Mulldist (CommRing→Ring P')
+
+ -- Sum of Zeros is Zero
+ ∑Zero : {n : ℕ} → (U : FinVec R n) → ((i : Fin n) → U i ≡ 0r) → ∑ U ≡ 0r
+ ∑Zero {zero} U f = refl
+ ∑Zero {suc n} U f =
+ ∑ U
+ ≡⟨ refl ⟩
+ (U zero + ∑ (λ i → U (suc i)) )
+ ≡⟨ cong (λ a → a + ∑ (λ i → U (suc i))) (f zero) ⟩
+ (0r + ∑ (λ i → U (suc i)))
+ ≡⟨ +Comm 0r (∑ (λ i → U (suc i))) ⟩
+ ∑ (λ i → U (suc i)) + 0r
+ ≡⟨ +IdR (∑ (λ i → U (suc i))) ⟩
+ ∑ (λ i → U (suc i))
+ ≡⟨ ∑Zero {n} ((λ i → U (suc i))) (λ i → f (suc i)) ⟩
+ 0r ∎
+
+ -- Summs are commutative
+ ∑Comm : {n m : ℕ} → (U : FinVec (FinVec R m) n) →
+ ∑ (λ i → ∑ (λ j → U i j )) ≡ ∑ (λ j → ∑ (λ i → U i j))
+ ∑Comm {zero} {zero} U = refl
+ ∑Comm {zero} {m} U =
+ 0r
+ ≡⟨ sym (∑Zero (λ (j : Fin m) → 0r) (λ (j : Fin m) → refl)) ⟩
+ ∑ (λ (j : Fin m) → 0r)
+ ≡⟨ ∑Compat (λ j → 0r) (λ j → ∑ (λ i → U i j )) (λ j → refl) ⟩
+ ( (∑ λ j → ∑ (λ i → U i j )))
+ ∎
+ ∑Comm {n} {zero} U =
+ ∑ (λ (i : Fin n) → 0r)
+ ≡⟨ ∑Zero ( (λ (i : Fin n) → 0r)) ( (λ i → refl)) ⟩
+ 0r
+ ∎
+ ∑Comm {suc n} {suc m} U =
+ ∑ (λ i → ∑ (U i))
+ ≡⟨ refl ⟩
+ ( ∑ (λ i → (U i zero + ∑ λ j → (U i (suc j)))) )
+ ≡⟨ bigOpSplit +Comm (λ i → U i zero) (λ i → ∑ λ j → (U i (suc j))) ⟩
+ (∑ (λ i → (U i zero)) + ∑ λ i → (∑ λ j → (U i (suc j))))
+ ≡⟨ cong (λ a → ∑ (λ i → (U i zero)) + a) (∑Comm λ i → ( λ j → (U i (suc j) ))) ⟩
+ (∑ (λ i → U i zero) + ∑ (λ j → ∑ (λ i → U i (suc j))))
+ ≡⟨ refl ⟩
+ ∑ (λ j → ∑ (λ i → U i j))
+ ∎
+
+ -- Indikator function: ind> i j = 1r if i>j and ind> i j = 0r else
+ ind> : (i j : ℕ) → R
+ ind> zero j = 0r
+ ind> (suc i) zero = 1r
+ ind> (suc i) (suc j) = ind> i j
+
+ ind>prop : {n m : ℕ} → (A B : FinVec (FinVec R m) n) →
+ ((i : Fin n) → (j : Fin m) → (toℕ j) <' (toℕ i) → A i j ≡ B i j) →
+ (i : Fin n) → (j : Fin m) →
+ (ind> (toℕ i) (toℕ j) · A i j) ≡ (ind> (toℕ i) (toℕ j) · B i j)
+ ind>prop {m = suc m} A B f zero j = solve! P'
+ ind>prop {m = suc m} A B f (suc i) zero =
+ cong
+ (λ a → 1r · a)
+ (f (suc i) zero (s≤s z≤))
+ ind>prop {m = suc m} A B f (suc i) (suc j) =
+ ind>prop
+ (λ i j → A (suc i) (suc j))
+ (λ i j → B (suc i) (suc j))
+ (λ i₁ j₁ le → f (suc i₁) (suc j₁)
+ (s≤s le))
+ i
+ j
+
+ ind>anti : {n m : ℕ} → (A B : FinVec (FinVec R m) n) →
+ ((i : Fin n) (j : Fin m) → (toℕ i) ≤' (toℕ j) → A i j ≡ B i j) →
+ (i : Fin n) → (j : Fin m) →
+ (1r + (- ind> (toℕ i) (toℕ j))) · A i j ≡ (1r + - (ind> (toℕ i) (toℕ j))) · B i j
+ ind>anti {m = suc m} A B f zero j =
+ cong
+ (λ a → (1r + - 0r) · a)
+ (f zero j z≤)
+ ind>anti {m = suc m} A B f (suc i) zero = solve! P'
+ ind>anti {m = suc m} A B f (suc i) (suc j) =
+ ind>anti
+ (λ i j → A (suc i) (suc j))
+ (λ i j → B (suc i) (suc j))
+ (λ i₁ j₁ le → f (suc i₁) (suc j₁) (s≤s le)) i j
+
+ ind>Neg : (i j : ℕ) → (1r + - ind> (suc i) j) ≡ ind> j i
+ ind>Neg i zero = +InvR 1r
+ ind>Neg zero (suc j) = solve! P'
+ ind>Neg (suc i) (suc j) = ind>Neg i j
+
+ ind>Suc : (i j : ℕ) → ind> (suc i) j ≡ (1r + - ind> j i)
+ ind>Suc i zero = solve! P'
+ ind>Suc zero (suc j) = solve! P'
+ ind>Suc (suc i) (suc j) = ind>Suc i j
+
+ --Index Shift--
+ ∑∑ShiftSuc : {n : ℕ} → (A : Fin (suc n) → Fin n → R) →
+ ∑ (λ (i : Fin (suc n)) → ∑ ( λ j → ind> (toℕ i) (toℕ j) · A i j))
+ ≡
+ ∑ (λ (i : Fin n) → ∑ ( λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j))
+ ∑∑ShiftSuc {zero} A = ∑Zero {one} (λ j → 0r) (λ j → refl)
+ ∑∑ShiftSuc {suc n} A =
+ ∑ {suc (suc n)}
+ (λ i →
+ ∑ (λ j → ind> (toℕ i) (toℕ j) · A i j))
+ ≡⟨ refl ⟩
+ ∑ {suc n}
+ (λ j → ind> zero (toℕ j) · A zero j)
+ + ∑ (λ i →
+ ∑ (λ j →
+ ind> (toℕ (suc i)) (toℕ j) · A (suc i) j))
+ ≡⟨
+ cong
+ (λ a → a + ∑ (λ i →
+ ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j)))
+ (∑Compat
+ (λ j → ind> zero (toℕ j) · A zero j)
+ (λ j → 0r)
+ (λ j → solve! P'))
+ ⟩
+ ∑ {suc n} (λ j → 0r) +
+ ∑ (λ i → ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j))
+ ≡⟨
+ cong
+ (λ a → a + ∑ (λ i → ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j)))
+ (∑Zero {suc n} (λ j → 0r) (λ j → refl)) ⟩
+ 0r + ∑ (λ i → ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j))
+ ≡⟨
+ +Comm
+ 0r
+ (∑ (λ i → ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j)))
+ ⟩
+ ∑ (λ i → ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j)) + 0r
+ ≡⟨
+ +IdR
+ (∑ (λ i → ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j)))
+ ⟩
+ ∑ (λ i → ∑ (λ j → ind> (toℕ (suc i)) (toℕ j) · A (suc i) j))
+ ∎
+
+ ∑∑ShiftWeak : {n : ℕ} → (A : Fin (suc n) → Fin n → R) →
+ ∑ (λ (i : Fin (suc n)) → ∑ ( λ j → (1r + - ind> (toℕ i) (toℕ j)) · A i j))
+ ≡
+ ∑ (λ (i : Fin n) →
+ ∑ ( λ j →
+ (1r + - ind> (toℕ (weakenFin i)) (toℕ j)) · A (weakenFin i) j))
+ ∑∑ShiftWeak {zero} A =
+ ∑Zero {one}
+ (λ i → ∑ ( λ j → (1r + - ind> (toℕ i) (toℕ j)) · A i j))
+ (λ i → refl)
+ ∑∑ShiftWeak {suc n} A =
+ (∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) +
+ ∑
+ (λ i → ∑ (λ j → (1r + - ind> (toℕ (suc i)) (toℕ j)) · A (suc i) j)))
+ ≡⟨
+ cong
+ (λ a → ∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) + a)
+ (∑Compat
+ (λ i → ∑ (λ j → (1r + - ind> (toℕ (suc i)) (toℕ j)) · A (suc i) j))
+ (λ i →
+ (1r + - ind> (toℕ (suc i)) zero) · A (suc i) zero +
+ ∑ (λ j → (1r + - ind> (toℕ (suc i)) (toℕ (suc j))) · A (suc i) (suc j)))
+ (λ i → refl))
+ ⟩
+ ∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) +
+ ∑ (λ i →
+ (1r + - ind> (toℕ (suc i)) zero) · A (suc i) zero +
+ ∑ (λ j →
+ (1r + - ind> (toℕ (suc i)) (toℕ (suc j))) · A (suc i) (suc j)))
+ ≡⟨
+ cong
+ (λ a → ∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) + a)
+ (∑Split
+ (λ i →
+ (1r + - ind> (toℕ (suc i)) zero) · A (suc i) zero)
+ (λ i →
+ ∑ (λ j →
+ (1r + - ind> (toℕ (suc i)) (toℕ (suc j)))
+ · A (suc i) (suc j))))
+ ⟩
+ (∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) +
+ (∑ (λ i → (1r + - ind> (toℕ (suc i)) zero) · A (suc i) zero) +
+ ∑
+ (λ i →
+ ∑ (λ j → (1r + - ind> (toℕ i) (toℕ j)) · A (suc i) (suc j)))))
+ ≡⟨
+ cong
+ (λ a →
+ ∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) +
+ (∑ (λ i →
+ (1r + - ind> (toℕ (suc i)) zero) ·
+ A (suc i) zero) + a))
+ (∑∑ShiftWeak (λ i j → A (suc i) (suc j)))
+ ⟩
+ (∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) +
+ (∑ (λ i → (1r + - ind> (toℕ (suc i)) zero) · A (suc i) zero) +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ (suc (weakenFin i))) (toℕ (suc j)))
+ · A (suc (weakenFin i)) (suc j)))))
+ ≡⟨
+ cong
+ (λ a →
+ (∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) +
+ (a +
+ ∑ (λ i →
+ ∑ (λ j →
+ (1r + - ind> (toℕ (suc (weakenFin i))) (toℕ (suc j)))
+ · A (suc (weakenFin i)) (suc j))))))
+ (
+ ∑ (λ i → (1r + - ind> (toℕ (suc i)) zero) · A (suc i) zero)
+ ≡⟨ refl ⟩
+ ∑ (λ i →
+ (1r + - 1r) · A (suc i) zero)
+ ≡⟨ ∑Compat (
+ λ i → (1r + - 1r) · A (suc i) zero)
+ (λ i → 0r)
+ (λ i → solve! P')
+ ⟩
+ ∑ (λ (i : Fin (suc n)) → 0r)
+ ≡⟨
+ ∑Zero
+ (λ (i : Fin (suc n)) → 0r)
+ (λ i → refl)
+ ⟩
+ 0r
+ ≡⟨ sym (∑Zero (λ (i : Fin n) → 0r) (λ i → refl)) ⟩
+ ∑ (λ (i : Fin n) → 0r)
+ ≡⟨ ∑Compat
+ (λ (i : Fin n) → 0r)
+ (λ i → (1r + - 1r) · A (suc (weakenFin i)) zero)
+ (λ i → solve! P')
+ ⟩
+ ∑ (λ i → (1r + - 1r) · A (suc (weakenFin i)) zero)∎
+ )⟩
+ (∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) +
+ (∑
+ (λ i →
+ (1r + - ind> (toℕ (suc (weakenFin i))) zero) ·
+ A (suc (weakenFin i)) zero)
+ +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ (suc (weakenFin i))) (toℕ (suc j))) ·
+ A (suc (weakenFin i)) (suc j)))))
+ ≡⟨
+ cong
+ (λ a → ∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) + a)
+ (sym
+ (∑Split
+ (λ i →
+ (1r + - ind> (toℕ (suc (weakenFin i))) zero) ·
+ A (suc (weakenFin i)) zero)
+ (λ i → ∑ (λ j →
+ (1r + - ind> (toℕ (suc (weakenFin i))) (toℕ (suc j))) ·
+ A (suc (weakenFin i)) (suc j)))))
+ ⟩
+ ∑ (λ j → (1r + - ind> zero (toℕ j)) · A zero j) +
+ ∑
+ (λ i →
+ ∑
+ (λ j →
+ (1r + - ind> (toℕ (suc (weakenFin i))) (toℕ j)) ·
+ A (suc (weakenFin i)) j)) ∎
diff --git a/dist-newstyle/cache/compiler b/dist-newstyle/cache/compiler
new file mode 100644
index 000000000..e680cec51
Binary files /dev/null and b/dist-newstyle/cache/compiler differ
diff --git a/dist-newstyle/cache/config b/dist-newstyle/cache/config
new file mode 100644
index 000000000..ac7ba02f1
Binary files /dev/null and b/dist-newstyle/cache/config differ
diff --git a/dist-newstyle/cache/elaborated-plan b/dist-newstyle/cache/elaborated-plan
new file mode 100644
index 000000000..bebc06a9d
Binary files /dev/null and b/dist-newstyle/cache/elaborated-plan differ
diff --git a/dist-newstyle/cache/improved-plan b/dist-newstyle/cache/improved-plan
new file mode 100644
index 000000000..a5bfebfff
Binary files /dev/null and b/dist-newstyle/cache/improved-plan differ
diff --git a/dist-newstyle/cache/plan.json b/dist-newstyle/cache/plan.json
new file mode 100644
index 000000000..f79bcfcd3
--- /dev/null
+++ b/dist-newstyle/cache/plan.json
@@ -0,0 +1 @@
+{"cabal-version":"3.10.3.0","cabal-lib-version":"3.10.3.0","compiler-id":"ghc-9.4.8","os":"linux","arch":"x86_64","install-plan":[{"type":"pre-existing","id":"array-0.5.4.0","pkg-name":"array","pkg-version":"0.5.4.0","depends":["base-4.17.2.1"]},{"type":"pre-existing","id":"base-4.17.2.1","pkg-name":"base","pkg-version":"4.17.2.1","depends":["ghc-bignum-1.3","ghc-prim-0.9.1","rts-1.0.2"]},{"type":"pre-existing","id":"bytestring-0.11.5.3","pkg-name":"bytestring","pkg-version":"0.11.5.3","depends":["base-4.17.2.1","deepseq-1.4.8.0","ghc-prim-0.9.1","template-haskell-2.19.0.0"]},{"type":"configured","id":"cubical-utils-1.0-inplace-Everythings","pkg-name":"cubical-utils","pkg-version":"1.0","flags":{},"style":"local","pkg-src":{"type":"local","path":"/home/fwiesnet/Agda/Cubical_new/cubical/."},"dist-dir":"/home/fwiesnet/Agda/Cubical_new/cubical/dist-newstyle/build/x86_64-linux/ghc-9.4.8/cubical-utils-1.0/x/Everythings","build-info":"/home/fwiesnet/Agda/Cubical_new/cubical/dist-newstyle/build/x86_64-linux/ghc-9.4.8/cubical-utils-1.0/x/Everythings/build-info.json","depends":["base-4.17.2.1","directory-1.3.7.1"],"exe-depends":[],"component-name":"exe:Everythings","bin-file":"/home/fwiesnet/Agda/Cubical_new/cubical/dist-newstyle/build/x86_64-linux/ghc-9.4.8/cubical-utils-1.0/x/Everythings/build/Everythings/Everythings"},{"type":"pre-existing","id":"deepseq-1.4.8.0","pkg-name":"deepseq","pkg-version":"1.4.8.0","depends":["array-0.5.4.0","base-4.17.2.1","ghc-prim-0.9.1"]},{"type":"pre-existing","id":"directory-1.3.7.1","pkg-name":"directory","pkg-version":"1.3.7.1","depends":["base-4.17.2.1","filepath-1.4.2.2","time-1.12.2","unix-2.7.3"]},{"type":"pre-existing","id":"filepath-1.4.2.2","pkg-name":"filepath","pkg-version":"1.4.2.2","depends":["base-4.17.2.1"]},{"type":"pre-existing","id":"ghc-bignum-1.3","pkg-name":"ghc-bignum","pkg-version":"1.3","depends":["ghc-prim-0.9.1"]},{"type":"pre-existing","id":"ghc-boot-th-9.4.8","pkg-name":"ghc-boot-th","pkg-version":"9.4.8","depends":["base-4.17.2.1"]},{"type":"pre-existing","id":"ghc-prim-0.9.1","pkg-name":"ghc-prim","pkg-version":"0.9.1","depends":["rts-1.0.2"]},{"type":"pre-existing","id":"pretty-1.1.3.6","pkg-name":"pretty","pkg-version":"1.1.3.6","depends":["base-4.17.2.1","deepseq-1.4.8.0","ghc-prim-0.9.1"]},{"type":"pre-existing","id":"rts-1.0.2","pkg-name":"rts","pkg-version":"1.0.2","depends":[]},{"type":"pre-existing","id":"template-haskell-2.19.0.0","pkg-name":"template-haskell","pkg-version":"2.19.0.0","depends":["base-4.17.2.1","ghc-boot-th-9.4.8","ghc-prim-0.9.1","pretty-1.1.3.6"]},{"type":"pre-existing","id":"time-1.12.2","pkg-name":"time","pkg-version":"1.12.2","depends":["base-4.17.2.1","deepseq-1.4.8.0"]},{"type":"pre-existing","id":"unix-2.7.3","pkg-name":"unix","pkg-version":"2.7.3","depends":["base-4.17.2.1","bytestring-0.11.5.3","time-1.12.2"]}]}
\ No newline at end of file
diff --git a/dist-newstyle/cache/solver-plan b/dist-newstyle/cache/solver-plan
new file mode 100644
index 000000000..9227feac8
Binary files /dev/null and b/dist-newstyle/cache/solver-plan differ
diff --git a/dist-newstyle/cache/source-hashes b/dist-newstyle/cache/source-hashes
new file mode 100644
index 000000000..7a00451d4
Binary files /dev/null and b/dist-newstyle/cache/source-hashes differ