\import Algebra.Algebra
\import Algebra.Group
\import Algebra.Group.Category
\import Algebra.Group.Symmetric
\import Algebra.Meta
\import Algebra.Module
\import Algebra.Module.LinearMap
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.RingHom
\import Algebra.Semiring
\import Arith.Fin
\import Arith.Int
\import Arith.Nat
\import Data.Array
\import Data.Fin (fsuc, fsuc/=)
\import Data.Or
\import Function.Meta
\import Logic
\import Meta
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Fin

\type Matrix (R : \Type) (n m : Nat) => Array (Array R m) n

\func mkMatrix {R : \Type} {n m : Nat} (f : Fin n -> Fin m -> R) : Matrix R n m
  => \new Array (Array R m) n \lam i => \new Array R m (f i)

\func makeMatrix {R : \Type} {n m : Nat} (M : Array (Array R m) n) : Matrix R n m => M

\func mkColumn {R : \Type} (l : Array R) : Matrix R l.len 
  => mkMatrix \lam i _ => l i

\func mkRow {R : \Type} (l : Array R) : Matrix R  l.len
  => mkMatrix \lam _ => l

\func addColumn {R : \Type} {n m : Nat} (l : Array R n) (M : Matrix R n m) : Matrix R n (suc m)
  => makeMatrix \lam j => l j :: M j

\func addRow {R : \Type} {n m : Nat} (l : Array R m) (M : Matrix R n m) : Matrix R (suc n) m
  => l :: M

\func blockMatrix {R : AddPointed} {n m n' m' : Nat} (A : Matrix R n m) (B : Matrix R n' m') : Matrix R (n + n') (m + m')
  => makeMatrix $ map {Array R m} (`++' replicate m' zro) A ++' map (replicate m zro ++') B
  \where {
    \lemma elem00 {A : Matrix R n m} {B : Matrix R n' m'} (i : Fin n) (j : Fin m) : blockMatrix A B (fin-inc i) (fin-inc j) = A i j
      => path (\lam k => ++'.++'_index-left {Array R (m + m')} k _) *> ++'.++'_index-left

    \lemma elem10 {A : Matrix R n m} {B : Matrix R n' m'} (i : Fin n') (j : Fin m) : blockMatrix A B (fin-raise i) (fin-inc j) = 
      => path (\lam k => ++'.++'_index-right {Array R (m + m')} k _) *> ++'.++'_index-left

    \lemma elem01 {A : Matrix R n m} {B : Matrix R n' m'} (i : Fin n) (j : Fin m') : blockMatrix A B (fin-inc i) (fin-raise j) = 
      => path (\lam k => ++'.++'_index-left {Array R (m + m')} k _) *> ++'.++'_index-right

    \lemma elem11 {A : Matrix R n m} {B : Matrix R n' m'} (i : Fin n') (j : Fin m') : blockMatrix A B (fin-raise i) (fin-raise j) = B i j
      => path (\lam k => ++'.++'_index-right {Array R (m + m')} k _) *> ++'.++'_index-right
  }

\lemma blockMatrix_minor {R : AddPointed} {n m n' m' : Nat} {A : Matrix R (suc n) (suc m)} {B : Matrix R n' m'} (i : Fin (suc n)) (j : Fin (suc m))
  : minor (blockMatrix A B) (fin-inc i) (fin-inc j) = blockMatrix (minor A i j) B
  => determinant.minor=minor' (blockMatrix A B) _ _ *> path (\lam i' => skip (map_++' (skip __ _) {map {Array R (suc m)} (`++' replicate m' zro) A} i') (fin-inc i)) *>
       \have | s1 => path (\lam i' => skip (map {Array R (suc m)} (\lam x => skip_++' {_} {_} {_} {x} {replicate m' zro} i') A) i) *> {Array (Array R (m + m')) n} inv (skip_map (\lam x => skip x j ++' replicate m' zro))
             | s2 => path (\lam i' => map (\lam l => (skip_++' {R} {_} {_} {replicate (suc m) zro} {l} {j} *> path (\lam i => skip_replicate {R} {m} zro {j} i ++' l)) i') B)
       \in matrixExt' $ skip_++' *> {Array (Array R (m + m')) (n + n')} path (\lam i' => s1 i' ++' s2 i')

\lemma blockMatrix_* {R : Ring} {n m n' m' k k' : Nat} (A : Matrix R n m) (B : Matrix R n' m') (C : Matrix R m k) (D : Matrix R m' k')
  : blockMatrix A B MatrixRing.product blockMatrix C D = blockMatrix (A MatrixRing.product C) (B MatrixRing.product D)
  => matrixExt \lam i j => R.BigSum-split *> \case ++'.split-index i, ++'.split-index j \with {
    | inl (i',p), inl (j',q) => rewrite (p,q) $ pmap2 (+) (cong $ ext \lam i => pmap2 (*) (blockMatrix.elem00 i' i) (blockMatrix.elem00 i j')) (R.BigSum_zro \lam j => pmap (_ *) (blockMatrix.elem10 j j') *> zro_*-right) *> zro-right *> inv (blockMatrix.elem00 {_} {_} {_} {_} {_} {A MatrixRing.product C} {B MatrixRing.product D} i' j')
    | inl (i',p), inr (j',q) => rewrite (p,q) $ pmap2 (+) (R.BigSum_zro \lam i => pmap (_ *) (blockMatrix.elem01 i j') *> zro_*-right) (R.BigSum_zro \lam j => pmap (`* _) (blockMatrix.elem01 i' j) *> zro_*-left) *> zro-right *> inv (blockMatrix.elem01 {_} {_} {_} {_} {_} {A MatrixRing.product C} {B MatrixRing.product D} i' j')
    | inr (i',p), inl (j',q) => rewrite (p,q) $ pmap2 (+) (R.BigSum_zro \lam i => pmap (`* _) (blockMatrix.elem10 i' i) *> zro_*-left) (R.BigSum_zro \lam j => pmap (_ *) (blockMatrix.elem10 j j') *> zro_*-right) *> zro-right *> inv (blockMatrix.elem10 {_} {_} {_} {_} {_} {A MatrixRing.product C} {B MatrixRing.product D} i' j')
    | inr (i',p), inr (j',q) => rewrite (p,q) $ pmap2 (+) (R.BigSum_zro \lam i => pmap (_ *) (blockMatrix.elem01 i j') *> zro_*-right) (cong $ ext \lam j => pmap2 (*) (blockMatrix.elem11 i' j) (blockMatrix.elem11 j j')) *> zro-left *> inv (blockMatrix.elem11 {_} {_} {_} {_} {_} {A MatrixRing.product C} {B MatrixRing.product D} i' j')
  }

\func block21Matrix {R : AddPointed} {n m k : Nat} (A : Matrix R n k) (B : Matrix R m k) : Matrix R (n + m) k
  => makeMatrix (A ++' B)

\lemma blockMatrix_*-left {R : Ring} {n m n' m' k : Nat} {A : Matrix R n m} {B : Matrix R n' m'} {C : Matrix R m k} {D : Matrix R m' k}
  : blockMatrix A B MatrixRing.product block21Matrix C D = block21Matrix (A MatrixRing.product C) (B MatrixRing.product D)
  => matrixExt \lam i j => R.BigSum-split *> \case ++'.split-index i \with {
    | inl (i',p) => rewrite p $ pmap2 (+) (pmap R.BigSum $ exts \lam j' => pmap2 (\lam x (y : Array R k) => x * y j) (blockMatrix.elem00 i' j') (++'.++'_index-left {Array R k})) (R.BigSum_zro \lam j' => pmap (`* _) (blockMatrix.elem01 i' j') *> zro_*-left) *> zro-right *> inv (pmap {Array R k} (__ j) (++'.++'_index-left {Array R k}))
    | inr (i',p) => rewrite p $ pmap2 (+) (R.BigSum_zro \lam j' => pmap (`* _) (blockMatrix.elem10 i' j') *> zro_*-left) (pmap R.BigSum $ exts \lam j' => pmap2 (\lam x (y : Array R k) => x * y j) (blockMatrix.elem11 i' j') (++'.++'_index-right {Array R k})) *> zro-left *> inv (pmap {Array R k} (__ j) (++'.++'_index-right {Array R k}))
  }

\func block12Matrix {R : AddPointed} {n m k : Nat} (A : Matrix R k n) (B : Matrix R k m) : Matrix R k (n + m)
  => makeMatrix \lam j => A j ++' B j

\lemma blockMatrix_*-right {R : Ring} {n m n' m' k : Nat} {A : Matrix R n m} {B : Matrix R n' m'} {C : Matrix R k n} {D : Matrix R k n'}
  : block12Matrix C D MatrixRing.product blockMatrix A B = block12Matrix (C MatrixRing.product A) (D MatrixRing.product B)
  => matrixExt \lam i j => R.BigSum-split *> \case ++'.split-index j \with {
    | inl (j',p) => rewrite p $ pmap2 (+) (pmap R.BigSum $ exts \lam i' => pmap2 (*) ++'.++'_index-left (blockMatrix.elem00 i' j')) (R.BigSum_zro \lam i' => pmap (_ *) (blockMatrix.elem10 i' j') *> zro_*-right) *> zro-right *> inv ++'.++'_index-left
    | inr (j',p) => rewrite p $ pmap2 (+) (R.BigSum_zro \lam i' => pmap (_ *) (blockMatrix.elem01 i' j') *> zro_*-right) (pmap R.BigSum $ exts \lam i' => pmap2 (*) ++'.++'_index-right (blockMatrix.elem11 i' j')) *> zro-left *> inv ++'.++'_index-right
  }

\func matrixExt {R : \Type} {n m : Nat} {M N : Matrix R n m} (p : \Pi (i : Fin n) (j : Fin m) -> M i j = N i j) : M = N
  => path (\lam i => mkMatrix (\lam j k => p j k i))

\func matrixExt' {R : \Type} {n m : Nat} {M N : Matrix R n m} (p : M = {Array (Array R m) n} N) : M = N
  => path (\lam i => p i)

\func matrix-map {A B : \Type} (f : A -> B) {n m : Nat} (M : Matrix A n m) : Matrix B n m
  => mkMatrix \lam i j => f (M i j)

\instance MatrixAbGroup (A : AbGroup) (n m : Nat) : AbGroup (Matrix A n m) \cowith
  | zro => mkMatrix \lam _ _ => zro
  | + M N => mkMatrix \lam i j => M i j + N i j
  | zro-left => matrixExt \lam i j => zro-left
  | +-assoc => matrixExt \lam i j => +-assoc
  | +-comm => matrixExt \lam i j => +-comm
  | negative M => mkMatrix \lam i j => negative (M i j)
  | negative-left => matrixExt \lam i j => negative-left

\instance MatrixModule (R : Ring) (n m : Nat) : LModule R \cowith
  | AbGroup => MatrixAbGroup R n m
  | *c a M => mkMatrix \lam i j => a * M i j
  | *c-assoc => matrixExt \lam i j => *-assoc
  | *c-ldistr => matrixExt \lam i j => ldistr
  | *c-rdistr => matrixExt \lam i j => rdistr
  | ide_*c => matrixExt \lam i j => ide-left
  \where {
    \func *c-gen {R : Ring} {M : LModule R} (a : R) {n m : Nat} (A : Matrix M n m) : Matrix M n m
      => mkMatrix \lam i j => a *c A i j
  }

\lemma block12_21_* {R : Ring} {n m k k' : Nat} (A : Matrix R k n) (B : Matrix R k m) (C : Matrix R n k') (D : Matrix R m k')
  : block12Matrix A B MatrixRing.product block21Matrix C D = A MatrixRing.product C + B MatrixRing.product D
  => matrixExt \lam i j => R.BigSum-split *> pmap2 (R.BigSum __ + R.BigSum __)
      (exts \lam k => pmap2 (*) ++'.++'_index-left  (path \lam i => ++'.++'_index-left  {Array R k'} i j))
      (exts \lam k => pmap2 (*) ++'.++'_index-right (path \lam i => ++'.++'_index-right {Array R k'} i j))

\func diagonal {R : AddPointed} (l : Array R) : Matrix R l.len l.len
  => mkMatrix \lam i j => \case decideEq i j \with {
    | yes _ => l i
    | no _ => zro
  }

\instance MatrixRing (R : Ring) (n : Nat) : Ring (Matrix R n n)
  | AbGroup => MatrixModule R n n
  | ide : Matrix R n n => diagonal (replicate n R.ide)
  | * => product
  | ide-left => product_ide-left
  | ide-right => product_ide-right
  | *-assoc => product-assoc _ _ _
  | ldistr => product-ldistr
  | rdistr => product-rdistr _ _
  \where {
    \open AddMonoid

    \func product-gen {R : Ring} {L : LModule R} {n m k : Nat} (M : Matrix R n m) (N : Matrix L m k) : Matrix L n k
      => mkMatrix \lam i k => BigSum \lam j => M i j *c N j k

    \func \infixl  product {R : Ring} {n m k : Nat} (M : Matrix R n m) (N : Matrix R m k) : Matrix R n k
      => mkMatrix \lam i k => BigSum \lam j => M i j * N j k

    \lemma product-gen_ide-left {R : Ring} {M : LModule R} {n m : Nat} (A : Matrix M n m) : product-gen ide A = A
      => matrixExt \lam i j => BigSum-unique i (\lam k i/=k => later $ rewrite (decideEq/=_reduce i/=k) M.*c_zro-left) *> rewrite (decideEq=_reduce idp) M.ide_*c

    \lemma product_ide-left {R : Ring} {n m : Nat} {A : Matrix R n m} : ide product A = A
      => product-gen_ide-left {_} {RingLModule R} _

    \lemma product_ide-right {R : Ring} {n m : Nat} {M : Matrix R n m} : M product ide = M
      => matrixExt \lam i j => BigSum-unique j (\lam k j/=k => later $ rewrite (decideEq/=_reduce (\lam t => j/=k (inv t))) R.zro_*-right) *> rewrite (decideEq=_reduce idp) ide-right

    \lemma product_zro-left {R : Ring} {n m k : Nat} (A : Matrix R m k) : zro product A = {Matrix R n k} zro
      => matrixExt \lam i j => BigSum_zro \lam k => zro_*-left

    \lemma product_zro-right {R : Ring} {n m k : Nat} (A : Matrix R n m) : A product zro = {Matrix R n k} zro
      => matrixExt \lam i j => BigSum_zro \lam k => zro_*-right

    \lemma product-gen-assoc {R : Ring} {M : LModule R} {n m k l : Nat} {A : Matrix R n m} {B : Matrix R m k} {C : Matrix M k l} : product-gen (A product B) C = product-gen A (product-gen B C)
      => matrixExt \lam j1 j2 => path (\lam i => BigSum (\lam j3 => M.*c_BigSum-rdistr {\lam j4 => A j1 j4 * B j4 j3} {C j3 j2} i)) *>
          M.BigSum-transpose _ *> pmap BigSum (arrayExt \lam j3 => pmap BigSum $ arrayExt \lam j4 => *c-assoc) *>
          inv (path (\lam i => BigSum (\lam j3 => M.*c_BigSum-ldistr {A j1 j3} {\lam j4 => B j3 j4 *c C j4 j2} i)))

    \lemma product-assoc {R : Ring} {n m k l : Nat} (A : Matrix R n m) (B : Matrix R m k) (C : Matrix R k l) : A product B product C = A product (B product C)
      => product-gen-assoc {_} {RingLModule R}

    \lemma product-gen-ldistr {R : Ring} {M : LModule R} {n m k : Nat} {A : Matrix R n m} {B C : Matrix M m k} : product-gen A (B + C) = product-gen A B + product-gen A C
      => matrixExt \lam i j => pmap BigSum (arrayExt \lam k => *c-ldistr) *> M.BigSum_+

    \lemma product-ldistr {R : Ring} {n m k : Nat} {A : Matrix R n m} {B C : Matrix R m k} : A product (B + C) = A product B + A product C
      => product-gen-ldistr {_} {RingLModule R}

    \lemma product-gen-rdistr {R : Ring} {M : LModule R} {n m k : Nat} (A B : Matrix R n m) {C : Matrix M m k} : product-gen (A + B) C = product-gen A C + product-gen B C
      => matrixExt \lam i j => pmap BigSum (arrayExt \lam k => *c-rdistr) *> M.BigSum_+

    \lemma product-rdistr {R : Ring} {n m k : Nat} (A B : Matrix R n m) {C : Matrix R m k} : (A + B) product C = A product C + B product C
      => product-gen-rdistr {_} {RingLModule R} A B

    \lemma product-gen_negative-left {R : Ring} {L : LModule R} {n m k : Nat} (M : Matrix R n m) (N : Matrix L m k) : product-gen (negative M) N = negative (product-gen M N)
      => matrixExt \lam i j => pmap BigSum (arrayExt \lam k => L.*c_negative-left) *> inv L.BigSum_negative

    \lemma product_negative-left {R : Ring} {n m k : Nat} {M : Matrix R n m} {N : Matrix R m k} : negative M product N = negative (M product N)
      => product-gen_negative-left {_} {RingLModule R} _ _

    \lemma product-gen_negative-right {R : Ring} {L : LModule R} {n m k : Nat} (M : Matrix R n m) (N : Matrix L m k) : product-gen M (negative N) = negative (product-gen M N)
      => matrixExt \lam i j => pmap BigSum (arrayExt \lam k => L.*c_negative-right) *> inv L.BigSum_negative

    \lemma product_negative-right {R : Ring} {n m k : Nat} {M : Matrix R n m} {N : Matrix R m k} : M product negative N = negative (M product N)
      => product-gen_negative-right {_} {RingLModule R} _ _

    \lemma product-gen_negative-rdistr {R : Ring} {M : LModule R} {n m k : Nat} (A B : Matrix R n m) {C : Matrix M m k} : product-gen (A - B) C = product-gen A C - product-gen B C
      => product-gen-rdistr A (negative B) *> pmap (product-gen A C +) (product-gen_negative-left B C)

    \lemma ide_generates {R : Ring} {n : Nat} : LModule.IsGenerated {ArrayLModule n (RingLModule R)} ide
      => \lam l => inP (l, arrayExt \lam j => inv $ ArrayLModule.BigSum-index *> R.BigSum-unique j (\lam i j/=i => later $ rewrite (decideEq/=_reduce \lam p => j/=i (inv p)) zro_*-right) *> rewrite (decideEq=_reduce idp) ide-right)

    -- | A recursive definition of the identity matrix is sometimes more convenient.
    \func ide' {R : Ring} {n : Nat} : Array (Array R n) n \elim n
      |  => nil
      | suc n => ( :: replicate n zro) :: map (\lam l => R.zro :: l) ide'

    \lemma ide=ide' {R : Ring} {n : Nat} : ide {R} {n} = ide' \elim n
      |  => idp
      | suc n => matrixExt \case \elim __, \elim __ \with {
        | ,  => idp
        | , suc j => idp
        | suc i,  => idp
        | suc i, suc j => (later $ cases (decideEq i j) \with {
          | yes e => rewrite (decideEq=_reduce $ pmap fsuc e) idp
          | no q => rewrite (decideEq/=_reduce $ fsuc/= q) idp
        }) *> pmap (__ i j) ide=ide'
      }
  }

\instance MatrixAlgebra (R : CRing) (n : Nat) : AAlgebra { | R => R }
  | Ring => MatrixRing R n
  | LModule => MatrixModule R n n
  | *c-comm-left  => product_*c-comm-left _
  | *c-comm-right => product_*c-comm-right
  \where {
    \lemma product_*c-comm-left {R : Ring} {n m k : Nat} {a : R} (A : Matrix R n m) {B : Matrix R m k}
      : a *c (A MatrixRing.product B) = (a *c A) MatrixRing.product B
      => matrixExt \lam i j => R.BigSum-ldistr *> path (\lam i' => R.BigSum \lam k => inv (R.*-assoc {a} {A i k} {B k j}) i')

    \lemma product_*c-comm-right {R : CRing} {n m k : Nat} {a : R} {A : Matrix R n m} {B : Matrix R m k}
      : a *c (A MatrixRing.product B) = A MatrixRing.product (a *c B)
      => matrixExt \lam i j => R.BigSum-ldistr *> path (\lam i' => R.BigSum \lam k => (equation : a * (A i k * B k j) = A i k * (a * B k j)) i')
  }

\func determinant {R : CRing} {n : Nat} (M : Matrix R n n)
  => R.FinSum \lam (e : Sym n) => sign e * R.BigProd (\lam j => M (e j) j)
  \where {
    \func minor {R : \Type} {n m : Nat} (M : Matrix R (suc n) (suc m)) (i0 : Fin (suc n)) (j0 : Fin (suc m)) : Matrix R n m
      => map (skip __ j0) (skip M i0)

    \func minorExt {R : \Type} {n m : Nat} {M M' : Array (Array R (suc m)) (suc n)} {i : Fin (suc n)} {j : Fin (suc m)}
                   (p : \Pi {i' : Fin (suc n)} {j' : Fin (suc m)} -> i' /= i -> j' /= j -> M i' j' = M' i' j')
      : minor M i j = minor M' i j \elim n, M, M', i
      | , l :: nil, l' :: nil,  => idp
      | suc n, l :: M, l' :: M',  => matrixExt \lam i' j' => path (\lam ii => skipExt (\lam k => p {suc i'} (\case __)) ii j')
      | suc n, l :: M, l' :: M', suc i => path (\lam ii => skipExt (\lam k => p {} (\case __)) ii :: minorExt (\lam q => p (fsuc/= q)) ii)

    \func minor' {R : \Type} {n m : Nat} (M : Matrix R (suc n) (suc m)) (i0 : Fin (suc n)) (j0 : Fin (suc m)) : Matrix R n m
      => skip (map (skip __ j0) M) i0

    \func minor=minor' {R : \Type} {n m : Nat} (M : Matrix R (suc n) (suc m)) (i0 : Fin (suc n)) (j0 : Fin (suc m)) : minor M i0 j0 = minor' M i0 j0
      => matrixExt (aux M i0 j0)
      \where {
        \func aux {R : \Type} {n m : Nat} (M : Matrix R (suc n) (suc m)) (i0 : Fin (suc n)) (j0 : Fin (suc m)) (i : Fin n) (j : Fin m)
          : skip (skip M i0 i) j0 j = skip {Array R m} (map (skip __ j0) M) i0 i j \elim n, M, i0, i
          | suc n, l :: M, , i => idp
          | suc n, l :: M, suc i0,  => idp
          | suc n, l :: M, suc i0, suc i => aux M i0 j0 i j
      }

    \func skip_transpose {R : \Type} {n m : Nat} {M : Array (Array R m) (suc n)} {i : Fin (suc n)}
      : transpose (skip M i) = map (skip __ i) (transpose M) \elim n, M, i
      | , l :: nil,  => idp
      | suc n, l :: M,  => idp
      | suc n, l :: M, suc i => matrixExt \lam i' => \case \elim __ \with {
        |  => idp
        | suc j' => aux
      }
      \where
        \func aux {R : \Type} {n m : Nat} {M : Array (Array R m) (suc n)} {i : Fin (suc n)} {i' : Fin m} {j' : Fin n}
          : skip {Array R m} M i j' i' = skip (M __ i') i j' \elim n, M, i, j'
          | suc n, l :: M, , j' => idp
          | suc n, l :: M, suc i,  => idp
          | suc n, l :: M, suc i, suc j' => aux

    \func minor_transpose {R : \Type} {n m : Nat} (M : Matrix R (suc n) (suc m)) {i : Fin (suc m)} {j : Fin (suc n)}
      : minor (transpose M) i j = transpose (minor M j i)
      => path (\lam i' => map (skip __ j) (pmap transpose skip_transpose i')) *> inv skip_transpose *> inv (pmap transpose (minor=minor' M j i))

    \lemma multilinear {R : CRing} {n : Nat} : isMultiLinear {R} {n} {ArrayLModule n (RingLModule R)} {RingLModule R} (\lam M => determinant M) \elim n
      |  => ()
      | suc n => transportInv (\lam d => isMultiLinear {R} (\lam M => d M)) (path \lam i M => determinantN.determinant=determinant0 {R} {n} {M} i) (determinantN.multilinear {R} {suc n} )

    \lemma alternating {R : CRing} {n : Nat} : isAlternating {R} {n} {ArrayLModule n (RingLModule R)} {RingLModule R} (\lam M => determinant M) \elim n
      |  => ((), \lam _ (t,_,_,_) => \case t)
      | suc n => transportInv (\lam d => isAlternating {R} (\lam M => d M)) (path \lam i M => determinantN.determinant=determinant0 {R} {n} {M} i) (determinantN.alternating {R} {suc n} )

    \lemma alternatingT {R : CRing} {n : Nat} : isAlternating {R} {n} (\lam M => determinant (transpose M))
      => transportInv (isAlternating {R}) (ext \lam M => determinant_transpose M) alternating

    \func minor00 {R : \Type} {n m : Nat} (M : Matrix R (suc n) (suc m)) : minor M   = mkMatrix \lam i j => M (suc i) (suc j)
      => matrixExt \lam i j => skip_0 *> rewrite skip_0 idp
  }

\func determinantN {R : CRing} {n : Nat} (k : Fin n) (M : Matrix R n n) : R \elim n
  |  => 
  | suc n => R.BigSum \lam i => M i k * R.pow -1 (i Nat.+ k) * determinant (minor M i k)
  \where {
    \open determinant
    \open skip
    \open ArrayLModule

    \lemma minor_insert {R : CRing} {n m : Nat} {i : Fin (suc n)} {x : Array R (suc m)} {l : Array (Array R (suc m)) n} {j : Fin (suc m)}
      : minor (insert x l i) i j = \new Array (Array R m) n (\lam i => skip (l i) j)
      => path (\lam i' => map (skip __ j) (skip_insert_= i'))

    \lemma aux/= {R : CRing} {n m : Nat} {j i : Fin (suc n)} (p : j /= i) {k : Fin (suc m)} {x : Array R (suc m)} {M : Array (Array R (suc m)) n}
      : insert {Array R (suc m)} x M j i k = M (newIndex (\lam q => p (inv q))) k \elim n, j, i, M
      | _, , , _ => absurd (p idp)
      | suc n, , suc i, y :: M => idp
      | suc n, suc j, , y :: M => idp
      | suc n, suc j, suc i, y :: M => aux/= (\lam q => p (pmap fsuc q))

    \lemma minor_replace {R : CRing} {n : Nat} {i k : Fin (suc n)} {M : Array (Array R (suc n)) (suc n)} {j : Fin (suc n)} {x : Array R (suc n)} (p : j /= i)
      : minor (replace M j x) i k = replace (minor M i k) (newIndex p) (skip x k)
      => path (\lam i => map (skip __ k) (skip_replace_/= p i)) *> pmap makeMatrix (map_replace (skip __ k))

    \lemma multilinear {R : CRing} {n : Nat} (k : Fin n) : isMultiLinear {R} {n} {ArrayLModule n (RingLModule R)} {RingLModule R} (\lam M => determinantN k M) \elim n
      |  => ()
      | suc n => isMultilinear_BigSum {R} {suc n} {ArrayLModule (suc n) (RingLModule R)} (\lam i M => M i k * R.pow -1 (i Nat.+ k) * determinant (minor M i k)) \lam i M j => \case decideEq j i \with {
        | yes e => \new LinearMap {
          | func-+ {a} {b} => rewrite e $ *-assoc *> pmap {Array R (suc n)} (__ k * _) (insert-index {Array R (suc n)}) *> rdistr *> pmap2 (+)
                                (pmap (\lam x => _ * (_ * determinant x)) (minor_insert *> inv minor_insert) *> inv (*-assoc *> pmap {Array R (suc n)} (__ k * _) (insert-index {Array R (suc n)})))
                                (pmap (\lam x => _ * (_ * determinant x)) (minor_insert *> inv minor_insert) *> inv (*-assoc *> pmap {Array R (suc n)} (__ k * _) (insert-index {Array R (suc n)})))
        | func-*c {r} {a} => rewrite e $ *-assoc *> pmap {Array R (suc n)} (__ k * _) (insert-index {Array R (suc n)}) *> *-assoc *> pmap (r *) (pmap (\lam x => _ * (_ * determinant x)) (minor_insert *> inv minor_insert) *> inv (*-assoc *> pmap {Array R (suc n)} (__ k * _) (insert-index {Array R (suc n)})))
        }
        | no q => \new LinearMap {
          | func-+ => rewrite (aux/= q, aux/= q, aux/= q) $ pmap (_ *) (inv (path (\lam i' => determinant (minor (replace_insert {_} {M} {j} {replicate (suc n) R.zro} i') i k))) *> pmap determinant (minor_replace q) *> later (rewrite skip_+ $ func-+ {isMultiLinear.toReplace {R} {_} {_} {n} determinant.multilinear _ _} *> pmap2 (determinant __ + determinant __) (inv (minor_replace q) *> path (\lam i' => minor (replace_insert i') i k)) (inv (minor_replace q) *> path (\lam i' => minor (replace_insert i') i k)))) *> ldistr
          | func-*c {r} {x} => rewrite (aux/= q, aux/= q) $ pmap (_ * _ * __) (inv (path (\lam i' => determinant (minor (replace_insert {_} {M} {j} {replicate (suc n) R.zro} i') i k))) *> pmap determinant (minor_replace q) *> later (rewrite skip_*c $ func-*c {isMultiLinear.toReplace {R} {_} {_} {n} determinant.multilinear _ _} *> pmap (r * determinant __) (inv (minor_replace q))) *> path (\lam i' => r * determinant (minor (replace_insert i') i k)) *> *-comm) *> inv *-assoc *> *-comm
        }
      }

    \lemma alternating {R : CRing} {n : Nat} (k : Fin n) : isAlternating {R} {n} {ArrayLModule n (RingLModule R)} {RingLModule R} (\lam M => determinantN k M) \elim n
      |  => ((), \lam _ => \case __.)
      | suc n => (multilinear k, \lam M => aux k M)
      \where {
        \open NatSemiring(<,suc<suc)
        \open FinLinearOrder (FinLinearOrderInst)

        \func permutation1 {R : \Type} {n : Nat} (j : Fin (suc n)) (l : Array R (suc n)) : Perm l (l j :: skip l j) \elim n, j, l
          | , , l => Perm.perm-refl
          | suc n, , l => Perm.perm-refl
          | suc n, suc j, a :: l => perm-trans (perm-:: idp (permutation1 j l)) (perm-swap idp idp idp)

        \func permutation {R : \Type} {n : Nat} {i j : Fin (suc n)} (p : i < j) (l : Array R (suc n)) (q : l i = l j) : Perm (skip l i) (skip l j) \elim n, i, j, p, l, q
          | , , , (), _, _
          | suc n, , suc j, _, a :: l, idp => permutation1 j l
          | suc n, suc i, suc j, suc<suc p, a :: l, q => perm-:: idp (permutation p l q)

        \lemma permutation1_inversions {R : \Type} {n : Nat} {j : Fin (suc n)} {l : Array R (suc n)} : Perm.inversions (permutation1 j l) = j \elim n, j, l
          | , , l => idp
          | suc n, , a :: l => Perm.inversions_perm-:: *> Perm.inversions_perm-refl
          | suc n, suc j, a :: l => pmap suc permutation1_inversions

        \lemma permutation_inversions {R : \Type} {n : Nat} {i j : Fin (suc n)} {p : i < j} {l : Array R (suc n)} {q : l i = l j} : Perm.inversions (permutation p l q) = j -' suc i \elim n, i, j, p, l, q
          | , , , (), _, _
          | suc n, , suc j, _, a :: l, idp => permutation1_inversions *> inv -'0
          | suc n, suc i, suc j, suc<suc p, a :: l, q => Perm.inversions_perm-:: *> permutation_inversions

        \lemma minor-lem {R : CRing} {n : Nat} {i j k : Fin (suc n)} {M : Matrix R (suc n) (suc n)} (i/=j : i /= j) (p : M i = M j)
          : pow -1 (i Nat.+ k) * determinant (minor M i k) + pow -1 (j Nat.+ k) * determinant (minor M j k) = 
          => \case LinearOrder.trichotomy i j \with {
            | less i<j => aux i<j p
            | Tri.equals i=j => absurd (i/=j i=j)
            | greater j<i => +-comm *> aux j<i (inv p)
          }
          \where
            \lemma aux {R : CRing} {n : Nat} {i j k : Fin (suc n)} {M : Matrix R (suc n) (suc n)} (i<j : i < j) (p : M i = M j)
              : pow -1 (i Nat.+ k) * determinant (minor M i k) + pow -1 (j Nat.+ k) * determinant (minor M j k) = 
              => rewrite (minor=minor', minor=minor', isAlternating.alternating_perm {R} determinant.alternating $ permutation i<j (map (skip __ k) M) $ pmap (skip __ k) p) $
                 rewriteI *-assoc $ inv rdistr *> pmap (`* _) (unfold Perm.sign $ rewrite (permutation_inversions, inv R.pow_+, inv R.pow_-1_+2)
                  \have s : i Nat.+ k Nat.+ (j -' suc i) Nat.+  = suc (j Nat.+ k) => pmap suc $ unpos $ pmap (pos (suc (i Nat.+ k)) +) (-'=- $ suc_<_<= i<j) *> linarith
                  \in pmap (R.pow -1 __ + _) s *> pmap (`+ _) R.negative_ide-right *> negative-left) *> zro_*-left

        \lemma minor-lem' {R : CRing} {n : Nat} {i j k : Fin (suc n)} {M : Matrix R (suc n) (suc n)} (i/=j : i /= j) (p : \Pi (k : Fin (suc n)) -> M k i = M k j)
          : pow -1 (k Nat.+ i) * determinant (minor M k i) + pow -1 (k Nat.+ j) * determinant (minor M k j) = 
          => pmap2 (+) (pmap2 (pow -1 __ * __) +-comm $ inv $ pmap determinant (minor_transpose M) *> determinant_transpose (minor M k i)) (pmap2 (pow -1 __ * __) +-comm $ inv $ pmap determinant (minor_transpose M) *> determinant_transpose (minor M k j)) *> minor-lem {R} {n} {i} {j} {k} {transpose M} i/=j (arrayExt p)

        \lemma aux {R : CRing} {n : Nat} (k : Fin n) (M : Matrix R n n) (t : \Sigma (i j : Fin n) (i < j) (M i = M j)) : determinantN k M =  \elim n
          |  => \case t.
          | suc n => R.BigSum-unique2 {\lam i => M i k * R.pow -1 (i Nat.+ k) * determinant (minor M i k)} t. (\lam i i/=t1 i/=t2 => pmap (_ *) (determinant.alternating. (minor M i k) (newIndex \lam p => i/=t1 (inv p), newIndex \lam p => i/=t2 (inv p), newIndex_< t., pmap (skip __ k) $ skip-index *> t. *> inv skip-index)) *> zro_*-right) *>
                      rewrite (pmap {Array R _} (__ k) t.) (pmap2 (+) *-assoc *-assoc *> inv ldistr *>  pmap (_ *) (minor-lem.aux t. t.) *> zro_*-right )
      }

    \lemma determinantN_ide {R : CRing} {n : Nat} (k : Fin n) : determinantN k (MatrixRing.ide {R} {n}) =  \elim n
      |  => idp
      | suc n => R.BigSum-unique {\lam i => MatrixRing.ide i k * R.pow -1 (i Nat.+ k) * determinant (minor MatrixRing.ide i k)} k (\lam j k/=j => rewrite (decideEq/=_reduce \lam p => k/=j $ inv p) simplify) *>
                  rewrite (decideEq=_reduce idp, ide-left) (pmap2 (*) R.pow_-1_even (pmap determinant (pmap (minor __ k k) MatrixRing.ide=ide' *> ide'_minor k *> inv MatrixRing.ide=ide') *> determinant_ide {R} {n}) *> ide-left)
      \where {
        \func double-skip {R : \Set} {n m : Nat} {M : Array (Array R n) (suc m)} {k : Fin (suc m)} {i : Fin m} {j : Fin n}
          : skip {Array R _} M k i j = skip (map {Array R n} (__ j) M) k i \elim m, M, k, i
          | suc m, l :: M, , i => idp
          | suc m, l :: M, suc k,  => idp
          | suc m, l :: M, suc k, suc i => double-skip

        \lemma ide'_minor {R : Ring} {n : Nat} (k : Fin (suc n)) : minor (MatrixRing.ide' {R}) k k = MatrixRing.ide' \elim n, k
          | , k => idp
          | suc n,  => idp
          | suc n, suc k => pmap makeMatrix $ pmap2 (::) (pmap (\lam l => R.ide :: l) (skip_replicate R.zro)) $ arrayExt \lam i => pmap2 (::) (double-skip *> pmap {Array R _} (__ i) (skip_replicate R.zro {k})) $ cong (arrayExt \lam j => double-skip *> inv double-skip) *> pmap {Matrix R n n} (__ i) (ide'_minor k)
      }

    \lemma =determinant {R : CRing} {n : Nat} {k : Fin n} {M : Matrix R n n} : determinantN k M = determinant M
      => alternating-unique {R} (alternating k) determinant.alternating MatrixRing.ide_generates (determinantN_ide k *> inv determinant_ide) M

    \open AbMonoid
    \open Monoid

    \lemma determinant=determinant0 {R : CRing} {n : Nat} {M : Matrix R (suc n) (suc n)} : determinant M = determinantN {R} {suc n}  M
      => \have t (e : Sym (suc n)) : BigProd (\lam j => minor M (e )  (Sym.reduce e j) j) = BigProd (\lam j => M (e (fsuc j)) (fsuc j)) => cong (ext \lam j => minor_Sym)
         \in FinSum (\lam (e : Sym (suc n)) => sign e * BigProd (\lam j => M (e j) j)) ==< pmap FinSum (ext \lam e => rewrite (t,R.pow_+) equation) *> inv (FinSum_Equiv symmetric-rec) >==
             FinSum (\lam (p : \Sigma (Fin (suc n)) (Sym n)) => M p.  * pow -1 p. * (sign p. * BigProd (\lam j => minor M p.  (p. j) j))) ==< inv FinSum-double >==
             FinSum (\lam i => FinSum (\lam (e : Sym n) => M i  * pow -1 i * (sign e * BigProd (\lam j => minor M i  (e j) j)))) ==< cong (ext \lam i => inv R.FinSum-ldistr) >==
             FinSum (\lam i => M i  * pow -1 i * determinant (minor M i )) ==< FinSum=BigSum >==
             R.BigSum (\lam i => M i  * pow -1 i * determinant (minor M i )) `qed
      \where {
        \func skip_skip {A : \Type} {n : Nat} {l : Array A (suc n)} {k j : Fin (suc n)} {d : k /= j} : skip l k (FinSet.skip k j d) = l j \elim n, l, k, j
          | n, l, ,  => absurd (d idp)
          | suc n, a :: l, , suc j => idp
          | suc n, a :: l, suc k,  => idp
          | suc n, a :: l, suc k, suc j => skip_skip

        \func minor_Sym {A : \Type} {n : Nat} {M : Matrix A (suc n) (suc n)} {e : Sym (suc n)} {j : Fin n} : minor M (e )  (Sym.reduce e j) j = M (e (suc j)) (suc j)
          => skip_0 *> pmap {Array A (suc n)} (__ (suc j)) (skip_skip {Array A (suc n)})
      }
  }

\lemma determinant00 {R : CRing} (A : Matrix R  ) : determinant A = 
  => determinant_ide

\lemma determinant11 {R : CRing} (A : Matrix R  ) : determinant A = A  
  => inv (determinantN.=determinant {R} {} {}) *> simplify (pmap (_ *) (determinant_ide {R} {}) *> ide-right)

\lemma determinant22 {R : CRing} {A : Matrix R  } : determinant A = A   * A   - A   * A  
  => inv (determinantN.=determinant {R} {} {}) *> simplify (pmap2 (+) (pmap (_ *) $ determinant11 (minor A  )) $
      pmap (\lam x => negative $ _ * x) (determinant11 (minor A  )))

\open determinant(minor)

\lemma determinant_ide {R : CRing} {n : Nat} : determinant (MatrixRing.ide {R} {n}) =  \elim n
  |  => \case R.FinSum_char _ \with {
    | inP p => p. *> zro-right *> ide-right
  }
  | suc n => rewrite determinantN.determinant=determinant0 (determinantN.determinantN_ide {R} {suc n} )
  \where {
    \lemma ide_minor {R : Ring} {n : Nat} : minor (MatrixRing.ide {R} {suc n})   =  \elim n
      |  => idp
      | suc n => matrixExt \lam i j => mcases {} \with {
        | yes p => rewrite (decideEq=_reduce $ pmap fsuc p) idp
        | no q => rewrite (decideEq/=_reduce $ fsuc/= q) idp
      }
  }

\lemma determinant_* {R : CRing} {n : Nat} {M N : Matrix R n n} : determinant (M * N) = determinant M * determinant N
  => alternating-unique {R}
      (isAlternating_linear-left {R} (\new LinearMap {
        | func (l : Array R n) => mkArray \lam k => R.BigSum \lam j => l j * N j k
        | func-+ => arrayExt \lam k => pmap R.BigSum (arrayExt \lam j => rdistr) *> R.BigSum_+
        | func-*c => arrayExt \lam k => pmap R.BigSum (arrayExt \lam j => *-assoc) *> inv R.BigSum-ldistr
      }) determinant.alternating)
      (isAlternating_linear-right {R} determinant.alternating RingLModule.*_hom-right)
      MatrixRing.ide_generates
      (pmap determinant ide-left *> inv (pmap (`* _) determinant_ide *> ide-left))
      M

\func transpose {R : \Type} {n m : Nat} (M : Matrix R n m) : Matrix R m n
  => mkMatrix (\lam i j => M j i)
  \where {
    \lemma isInv {R : CRing} {n : Nat} (A : Monoid.Inv {MatrixRing R n}) : Monoid.Inv (transpose A.val)
      => determinant-inv. $ transportInv Monoid.Inv (later $ determinant_transpose A.val) (determinant-inv. A)
  }

\lemma determinant_transpose {R : CRing} {n : Nat} (M : Matrix R n n) : determinant (transpose M) = determinant M
  => R.FinSum_Equiv SymmetricGroup.inv-isEquiv *> pmap R.FinSum (ext \lam (e : Sym n) => pmap2 (*) sign_inverse $ CMonoid.BigProd_Perm $ transport (Perm _) (arrayExt \lam j => later $ pmap (M (e j)) (e.ret_f j)) (Perm.equiv_perm e))

\func adjugate {R : CRing} {n : Nat} (M : Matrix R n n) : Matrix R n n \elim n
  |  => M
  | suc n => mkMatrix \lam i j => Monoid.pow -1 (j + i) * determinant (minor M j i)

\lemma adjugate_transpose {R : CRing} {n : Nat} (M : Matrix R n n) : adjugate (transpose M) = transpose (adjugate M) \elim n
  |  => idp
  | suc n => matrixExt \lam i j => pmap2 (R.pow -1 __ * __) +-comm $ pmap determinant (determinant.minor_transpose M) *> determinant_transpose (minor M i j)

\lemma adjugate-left {R : CRing} {n : Nat} {M : Matrix R n n} : adjugate M * M = determinant M *c 
  => matrixExt \lam i k => mcases \with {
       | yes p => rewrite p determinant_adjugate_= *> inv ide-right
       | no q => determinant_adjugate_/= q *> inv zro_*-right
     }
  \where {
    \lemma determinant_adjugate_= {R : CRing} {n : Nat} {M : Matrix R n n} {k : Fin n} : R.BigSum (\lam j => adjugate M k j * M j k) = determinant M \elim n
      | suc n => path (\lam i => R.BigSum (\lam (j : Fin (suc n)) => (R.*-comm {R.pow -1 (j Nat.+ k) * determinant (minor M j k)} {M j k} *> inv *-assoc) i)) *> determinantN.=determinant

    \lemma adjugate-lem {R : CRing} {n : Nat} {M : Matrix R n n} {i i' j : Fin n} (i/=i' : i /= i') (p : \Pi (k : Fin n) -> M k i = M k i') : negative (adjugate M i j) = adjugate M i' j \elim n
      | suc n => AddMonoid.negative-unique (adjugate M i j) negative-left (determinantN.alternating.minor-lem' i/=i' p)

    \lemma adjugateExt {R : CRing} {n : Nat} {M M' : Matrix R n n} {i j : Fin n} (p : \Pi {i' j' : Fin n} -> i' /= i -> j' /= j -> M i' j' = M' i' j') : adjugate M j i = adjugate M' j i \elim n
      | suc n => pmap (R.pow -1 (i Nat.+ j) * determinant __) (determinant.minorExt p)

    \lemma determinant_adjugate_/= {R : CRing} {n : Nat} {M : Matrix R n n} {i k : Fin n} (i/=k : i /= k) : R.BigSum (\lam j => adjugate M i j * M j k) = 
      => \let | M' => mkMatrix \lam i' j' => \case decideEq i j' \with {
                      | yes _ => M i' k
                      | no _ => M i' j'
                    }
              | r : R.BigSum (\lam j => adjugate M' k j * M' j k) =  => determinant_adjugate_= *> inv (determinant_transpose M') *>
                      isAlternating.to/= {R} determinant.alternating (transpose M') (i, k, i/=k, arrayExt \lam j => rewrite (decideEq=_reduce idp, decideEq/=_reduce i/=k) idp)
         \in pmap R.BigSum (arrayExt \lam j => pmap2 (*) (adjugateExt (\lam p q => later $ rewrite (decideEq/=_reduce $ /=-sym q) idp) *> inv (adjugate-lem (/=-sym i/=k) \lam j => later $ rewrite (decideEq/=_reduce i/=k, decideEq=_reduce idp) idp)) (later $ rewrite (decideEq/=_reduce i/=k) idp) *> R.negative_*-left) *> inv R.BigSum_negative *> pmap negative r *> R.negative_zro
  }

\lemma transpose_* {R : CRing} {n : Nat} {M M' : Matrix R n n} : transpose (M * M') = transpose M' * transpose M
  => product
  \where
    \lemma product {R : CRing} {n m k : Nat} {M : Matrix R n m} {M' : Matrix R m k} : transpose (M MatrixRing.product M') = transpose M' MatrixRing.product transpose M
      => matrixExt \lam i j => cong $ ext \lam k => *-comm

\lemma adjugate-right {R : CRing} {n : Nat} {M : Matrix R n n} : M * adjugate M = determinant M *c 
  => pmap (M *) (adjugate_transpose (transpose M)) *> inv (transpose_* {R} {n} {adjugate (transpose M)} {transpose M}) *> pmap transpose adjugate-left *> matrixExt (\lam i j => pmap2 (*) (determinant_transpose M) $ later $ mcases {} \with {
    | yes p => rewrite (decideEq=_reduce (inv p)) idp
    | no q => rewrite (decideEq/=_reduce (/=-sym q)) idp
  })

\lemma determinant-inv {R : CRing} {n : Nat} {M : Matrix R n n} : Inv M <-> Inv (determinant M)
  => (\lam (c : Inv M) => Inv.lmake (determinant c.inv) $ inv determinant_* *> pmap determinant c.inv-left *> determinant_ide,
      \lam (c : Inv (determinant M)) => \new Inv {
        | inv => c.inv *c adjugate M
        | inv-left => inv *c-comm-left *> pmap (c.inv *c) adjugate-left *> inv (*c-assoc {_} {_} {_} {ide}) *> pmap (`*c ide) c.inv-left *> ide_*c
        | inv-right => inv *c-comm-right *> pmap (c.inv *c) adjugate-right *> inv (*c-assoc {_} {_} {_} {ide}) *> pmap (`*c ide) c.inv-left *> ide_*c
      })
  \where \open Monoid

\lemma matirx-inv {R : CRing} {n : Nat} {A : Matrix R n n} {B : Matrix R n n} (p : A * B = ) : Monoid.Inv B
  => determinant-inv. (Monoid.Inv.lmake (determinant A) $ inv determinant_* *> pmap determinant p *> determinant_ide)

\lemma determinant1_Inv {R : CRing} {n : Nat} (A : Matrix R n n) (p : determinant A = ) : Monoid.Inv A
  => determinant-inv. $ transportInv Monoid.Inv p Monoid.Inv.ide-isInv

\lemma blockMatrix_Inv {R : CRing} {n m : Nat} {A : Matrix R n n} {B : Matrix R m m} : Inv (blockMatrix A B) <-> (\Sigma (Inv A) (Inv B))
  => (\lam s => (determinant-inv. $ Inv.cfactor-left $ transport Inv (determinant_block A B) $ determinant-inv. s,
                 determinant-inv. $ Inv.cfactor-right $ transport Inv (determinant_block A B) $ determinant-inv. s),
      \lam s => determinant-inv. $ transportInv Inv (determinant_block A B) $ Inv.product (determinant-inv. s.) (determinant-inv. s.))
  \where \open Monoid

\lemma determinant_map {R S : CRing} (f : RingHom R S) {n : Nat} (A : Matrix R n n) : f (determinant A) = determinant (matrix-map f A)
  => AddMonoidHom.func-FinSum f *> pmap AbMonoid.FinSum (ext \lam e => func-* *> pmap2 (*) (sign.sign_hom f) MonoidHom.func-BigProd)

\lemma determinant_block {R : CRing} {n m : Nat} (A : Matrix R n n) (B : Matrix R m m) : determinant (blockMatrix A B) = determinant A * determinant B \elim n
  |  => inv (pmap (`* _) (determinant00 A) *> ide-left)
  | suc n => inv (determinantN.=determinant {R} {suc (n + m)} {} {blockMatrix A B}) *>
      (cong (++'-split {R} {suc n} *> pmap2 (::) (pmap (_ *) (pmap determinant (blockMatrix_minor  ) *> determinant_block (minor A  ) B) *> inv *-assoc)
                                           (cong (ext \lam j => pmap2 (*) (pmap2 (*) (blockMatrix.elem00 {R} {suc n} {suc n} (suc j) ) $ later $ rewrite fin-inc.char idp) (pmap determinant (blockMatrix_minor (suc j) ) *> determinant_block (minor A (suc j) ) B) *> inv *-assoc)
                                                 (exts \lam j => *-assoc *> pmap (`* _) (blockMatrix.elem10 {R} {suc n} {suc n} j ) *> zro_*-left)))
            *> R.BigSum_++' {\lam i => A i  * R.pow -1 i * determinant (minor A i ) * determinant B} *> pmap (_ +) (R.BigSum_replicate0 {m}) *> zro-right
        : R.BigSum (\lam i => blockMatrix A B i  * R.pow -1 i * determinant (minor (blockMatrix A B) i )) = R.BigSum (\lam i => A i  * R.pow -1 i * determinant (minor A i ) * determinant B))
      *> inv (R.BigSum-rdistr {\lam i => A i  * R.pow -1 i * determinant (minor A i )}) *> pmap (`* _) (determinantN.=determinant {R} {suc n} {})

{- | If {M} is an R-module, {U} is a matrix over {M}, and {A} is a matrix over {R} such that `A * U = 0`, then `determinant A *c U = 0`.
 -
 -   This lemma easily follows from the equation `adjugate A * A = determinant A *c ide`, but has some interesting consequences:
 -   * Eigenvalues of a matrix `B` are roots of its charachteristic polynomial (see {eigen-root}).
 -     Indeed, if we take `M := R` and `A := b *c ide - B`, then the assumption says that
 -     `b` is an eigenvalue of `B` (with {U} being its eigenvector) and the conclusion implies that `b` a root of `charPoly B`.
 -   * Nakayama's lemma (see {nakayama}).
 -   * Cayley–Hamilton theorem (see {cayley-hamilton}): if `B` is a matrix over a ring `S`, then `B` satisfies its own charachteristic polynomial.
 -     Indeed, if we take `R := S[X]`, `M := S^n` with `p *c U := p(B) * U`, and `A := X *c ide - B`, then `A * U = 0` for all `U`.
 -     Let `p := charPoly B` (which is equal to `determinant A`). Then `p(B) * U = p *c U = 0` for all `U`, which implies `p(B) = 0`.
 -}
\lemma equations-determinant {R : CRing} {M : LModule R} {n k : Nat} (A : Matrix R n n) {U : Matrix M n k}
                             (p : product-gen A U = ) : MatrixModule.*c-gen (determinant A) U = 
  => \have | r : product-gen (adjugate A)  =  => matrixExt \lam i j => M.BigSum_zro \lam k => M.*c_zro-right
           | t : product-gen (determinant A *c ide) U = 
               => pmap (product-gen __ U) (inv adjugate-left) *> product-gen-assoc *> cong p *> r
     \in matrixExt \lam i j => pmap (`*c _) (inv ide-right) *> (rewrite (decideEq=_reduce idp) in inv (M.BigSum-unique i \lam k i/=k => later $ rewrite (decideEq/=_reduce i/=k) $ pmap (`*c _) R.zro_*-right *> M.*c_zro-left) *> path (\lam i' => t i' i j))
  \where \open MatrixRing

\type IsDiagonal {R : AddPointed} {n m : Nat} (A : Matrix R n m) : \Prop
  => \Pi {i : Fin n} {j : Fin m} -> i /= {Nat} j -> A i j = 
  \where {
    \lemma transposed {R : AddPointed} {n m : Nat} {A : Matrix R n m} (d : IsDiagonal A) : IsDiagonal (transpose A)
      => \lam i/=j => d (/=-sym i/=j)

    \lemma =>upperTriangular {R : AddPointed} {n m : Nat} {A : Matrix R n m} (d : IsDiagonal A) : IsUpperTriangular A
      => \lam i j j<i => d \lam p => linarith

    \lemma =>lowerTriangular {R : AddPointed} {n m : Nat} {A : Matrix R n m} (d : IsDiagonal A) : IsLowerTriangular A
      => \lam i j j<i => d \lam p => linarith
  }

\lemma *c_IsDiagonal {R : Ring} {n m : Nat} {A : Matrix R n m} {a : R} (Ad : IsDiagonal A) : IsDiagonal (a *c A)
  => \lam i/=j => pmap (a *) (Ad i/=j) *> zro_*-right

\type IsUpperTriangular {R : AddPointed} {n m : Nat} (A : Matrix R n m) : \Prop
  => \Pi (i : Fin n) (j : Fin m) -> (j : Nat) < i -> A i j = 

\type IsLowerTriangular {R : AddPointed} {n m : Nat} (A : Matrix R n m) : \Prop
  => \Pi (i : Fin n) (j : Fin m) -> (i : Nat) < j -> A i j = 

\lemma diagonal-isDiagonal {R : AddPointed} {l : Array R} : IsDiagonal (diagonal l)
  => \lam {i} {j} q => rewrite (decideEq/=_reduce \lam (p : i = j) => q p) idp

\lemma determinant_IsUpperTriangular {R : CRing} {n : Nat} {A : Matrix R n n} (d : IsUpperTriangular A) : determinant A = R.BigProd (\lam j => A j j) \elim n
  |  => determinant00 A
  | suc n => inv (determinantN.=determinant {R} {suc n} {}) *> pmap2 (+)
              (pmap2 (*) ide-right $ pmap determinant (determinant.minor00 _) *> determinant_IsUpperTriangular {R} {n} {mkMatrix \lam i j => A (suc i) (suc j)} \lam i j i<j => d (suc i) (suc j) (NatSemiring.suc<suc i<j))
              (R.BigSum_zro \lam j => later $ rewrite (d (suc j) zro NatSemiring.zero<suc, zro_*-left) zro_*-left) *> zro-right

\lemma determinant_IsLowerTriangular {R : CRing} {n : Nat} {A : Matrix R n n} (d : IsLowerTriangular A) : determinant A = R.BigProd (\lam j => A j j)
  => inv (determinant_transpose A) *> determinant_IsUpperTriangular {_} {_} {transpose A} (\lam i j => d j i)

\lemma determinant_IsDiagonal {R : CRing} {n : Nat} {A : Matrix R n n} (d : IsDiagonal A) : determinant A = R.BigProd (\lam j => A j j)
  => determinant_IsUpperTriangular (IsDiagonal.=>upperTriangular d)

\lemma determinant_diagonal {R : CRing} {l : Array R} : determinant (diagonal l) = R.BigProd l
  => determinant_IsDiagonal {R} {l.len} {diagonal l} diagonal-isDiagonal *> pmap R.BigProd (exts \lam j => rewrite (decideEq=_reduce idp) idp)

\lemma determinant-nonSquare {R : CRing} {n m : Nat} (m<n : m < n) {A : Matrix R n m} {B : Matrix R m n} : determinant (A MatrixRing.product B) = 
  => \have r : \Pi (A : Matrix R n m) (B : Matrix R m n) -> determinant (A MatrixRing.product B) = 
             => rewriteI (<=_exists (LinearOrder.<_<= m<n), NatSemiring.+-comm) \lam A B => determinant-nonSquare_+ \lam p => linarith (-'_<= p)
     \in r A B
  \where {
    \lemma determinant-nonSquare_+ {R : CRing} {n k : Nat} (k/=0 : k /= ) {A : Matrix R (k + n) n} {B : Matrix R n (k + n)} : determinant (A MatrixRing.product B) =  =>
      \let | A' => block12Matrix  A
           | B' => block21Matrix  B
           | p : A' * B' = A MatrixRing.product B => block12_21_*  A  B *> cong (MatrixRing.product_zro-left ) *> zro-left
      \in pmap determinant (inv p) *> determinant_* {_} {_} {A'} {B'} *> pmap (`* _) (determinant_block12 k/=0 A) *> zro_*-left

    \lemma determinant_block12 {R : CRing} {n k : Nat} (k/=0 : k /= ) (A : Matrix R (k + n) n) : determinant (block12Matrix  A) =  \elim k
      |  => absurd (k/=0 idp)
      | suc k => inv (determinantN.=determinant {_} {suc k + n} {} {block12Matrix {R} {suc k}  A}) *> pmap2 (+) (*-assoc *> zro_*-left) (R.BigSum_zro \lam j => *-assoc *> zro_*-left) *> zro-left
  }

\lemma matrix-split-trivial {R : CRing} {n m : Nat} (m<n : m < n) {A : Matrix R n m} {B : Matrix R m n} (p : A MatrixRing.product B = ide) :  = {R} 
  => inv (determinant-nonSquare m<n) *> pmap determinant p *> determinant_ide

\lemma matrix-split_<= {R : NonZeroCRing} {n m : Nat} {A : Matrix R n m} {B : Matrix R m n} (p : A MatrixRing.product B = ide) : n <= m
  => \case LinearOrder.dec<_<= m n \with {
    | inl m<n => absurd $ zro/=ide $ matrix-split-trivial m<n p
    | inr n<=m => n<=m
  }