Theme/Det.lean — FrcCore

1import FrcCore.Theme.Hermitian2/-!3# FrcCore.Theme.Det — the determinant over the coefficient field (the operator theme)45The determinant of a square matrix over `K = 𝔽_p(√ν)` (the list matrices `Mat p ν` of `Theme/Dirac`), by Laplace6expansion along the first column: `det (r₀ :: …) = Σ_i (−1)^i · (row i)₀ · det (minor i)`, the minor the rows other7than `i` without their heads. The expansion along the first column makes the row lemmas inductions on the matrix:8linearity in each row, the sign change under an adjacent swap, the vanishing on two equal rows, the invariance under9adding a multiple of one row to another. `Theme/Elim.lean` continues with Gaussian elimination, which computes the10determinant with `n³` operations and is proved equal to `det`. Written for 8:T1 (the admissible set of Cayley11parameters, 7 November 2026). No axioms.12-/13namespace FRC.Dirac.Det1415open FRC FRC.Extension FRC.Dirac FRC.Dirac.Hermitian16open FRC.Dirac.Mat (nth)1718variable {p : Nat} [Pos p] {ν : Shell p}1920/-! ## Lists: rows, removal, length -/2122/-- The row `i` of a matrix (the empty row beyond the end) and the head of a row (`0` for the empty row). -/23def row (M : Mat p ν) (i : Nat) : List (Ext p ν) := nth [] M i24def head (r : List (Ext p ν)) : Ext p ν := nth 0 r 02526/-- The list without its `i`-th entry. -/27def removeAt {α : Type} : List α → Nat → List α28  | [], _ => []29  | _ :: l, 0 => l30  | a :: l, i + 1 => a :: removeAt l i3132/-- The list with its `i`-th entry replaced. -/33def setAt {α : Type} : List α → Nat → α → List α34  | [], _, _ => []35  | _ :: l, 0, x => x :: l36  | a :: l, i + 1, x => a :: setAt l i x3738theorem length_map {α β : Type} (f : α → β) : ∀ l : List α, (l.map f).length = l.length39  | [] => rfl40  | _ :: l => congrArg (· + 1) (length_map f l)4142theorem eq_zero_of_lt_one {n : Nat} (h : n < 1) : n = 0 := Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.zero_le _)43theorem sub_pos_of_lt' {m n : Nat} (h : m < n) : 0 < n - m := FRC.Nat.le_sub_of_add_le (by rw [Nat.add_comm]; exact h)4445theorem length_removeAt {α : Type} : ∀ (l : List α) (i : Nat), i < l.length → (removeAt l i).length + 1 = l.length46  | [], _, h => absurd h (Nat.not_lt_zero _)47  | _ :: _, 0, _ => rfl48  | _ :: l, i + 1, h => congrArg (· + 1) (length_removeAt l i (Nat.lt_of_succ_lt_succ h))4950theorem length_setAt {α : Type} : ∀ (l : List α) (i : Nat) (x : α), (setAt l i x).length = l.length51  | [], _, _ => rfl52  | _ :: _, 0, _ => rfl53  | _ :: l, i + 1, x => congrArg (· + 1) (length_setAt l i x)5455theorem nth_setAt_eq {α : Type} (d : α) : ∀ (l : List α) (i : Nat) (x : α), i < l.length → nth d (setAt l i x) i = x56  | [], _, _, h => absurd h (Nat.not_lt_zero _)57  | _ :: _, 0, _, _ => rfl58  | _ :: l, i + 1, x, h => nth_setAt_eq d l i x (Nat.lt_of_succ_lt_succ h)5960theorem nth_setAt_ne {α : Type} (d : α) : ∀ (l : List α) (i j : Nat) (x : α), i ≠ j → nth d (setAt l i x) j = nth d l j61  | [], _, _, _, _ => rfl62  | _ :: _, 0, 0, _, h => absurd rfl h63  | _ :: _, 0, _ + 1, _, _ => rfl64  | _ :: _, _ + 1, 0, _, _ => rfl65  | _ :: l, i + 1, j + 1, x, h => nth_setAt_ne d l i j x (fun e => h (congrArg (· + 1) e))6667/-- Removing entry `j` of `setAt l i x`: the entry `i` survives at `i` (`j > i`) or at `i − 1` (`j < i`). -/68theorem removeAt_setAt_gt {α : Type} : ∀ (l : List α) (i j : Nat) (x : α), i < j →69    removeAt (setAt l i x) j = setAt (removeAt l j) i x70  | [], _, _, _, _ => rfl71  | _ :: _, 0, 0, _, h => absurd h (Nat.lt_irrefl 0)72  | _ :: _, 0, _ + 1, _, _ => rfl73  | _ :: _, _ + 1, 0, _, h => absurd h (Nat.not_lt_zero _)74  | _ :: l, i + 1, j + 1, x, h => congrArg (_ :: ·) (removeAt_setAt_gt l i j x (Nat.lt_of_succ_lt_succ h))7576theorem removeAt_setAt_lt {α : Type} : ∀ (l : List α) (i j : Nat) (x : α), j < i →77    removeAt (setAt l i x) j = setAt (removeAt l j) (i - 1) x78  | [], _, _, _, _ => rfl79  | _ :: _, 0, _, _, h => absurd h (Nat.not_lt_zero _)80  | _ :: _, _ + 1, 0, _, _ => rfl81  | a :: l, i + 1, j + 1, x, h =>82    match i, Nat.lt_of_succ_lt_succ h with83    | 0, h' => absurd h' (Nat.not_lt_zero _)84    | i' + 1, h' => congrArg (a :: ·) (removeAt_setAt_lt l (i' + 1) j x h')8586theorem removeAt_setAt_eq {α : Type} : ∀ (l : List α) (i : Nat) (x : α), removeAt (setAt l i x) i = removeAt l i87  | [], _, _ => rfl88  | _ :: _, 0, _ => rfl89  | _ :: l, i + 1, x => congrArg (_ :: ·) (removeAt_setAt_eq l i x)9091theorem map_removeAt {α β : Type} (f : α → β) : ∀ (l : List α) (i : Nat), (removeAt l i).map f = removeAt (l.map f) i92  | [], _ => rfl93  | _ :: _, 0 => rfl94  | _ :: l, i + 1 => congrArg (_ :: ·) (map_removeAt f l i)9596theorem map_setAt {α β : Type} (f : α → β) : ∀ (l : List α) (i : Nat) (x : α), (setAt l i x).map f = setAt (l.map f) i (f x)97  | [], _, _ => rfl98  | _ :: _, 0, _ => rfl99  | _ :: l, i + 1, x => congrArg (_ :: ·) (map_setAt f l i x)100101theorem nth_map {α β : Type} (f : α → β) (d : α) : ∀ (l : List α) (i : Nat), nth (f d) (l.map f) i = f (nth d l i)102  | [], _ => rfl103  | _ :: _, 0 => rfl104  | _ :: l, i + 1 => nth_map f d l i105106-- appending, mapping and zipping (the core's `List.length_append`, `List.append_assoc`, `List.map_append`,107-- `List.length_zipWith` carry `propext`)108-- lists (the core's `List.length_append`, `List.append_assoc`, `List.map_append` carry `propext`)109theorem length_append' {α : Type} : ∀ (l m : List α), (l ++ m).length = l.length + m.length110  | [], m => (Nat.zero_add _).symm111  | _ :: l, m => by112    show (l ++ m).length + 1 = l.length + 1 + m.length113    rw [length_append' l m, Nat.add_right_comm]114115theorem append_assoc' {α : Type} : ∀ (l m k : List α), l ++ m ++ k = l ++ (m ++ k)116  | [], _, _ => rfl117  | _ :: l, m, k => congrArg (_ :: ·) (append_assoc' l m k)118119theorem map_append' {α β : Type} (f : α → β) : ∀ (l m : List α), (l ++ m).map f = l.map f ++ m.map f120  | [], _ => rfl121  | _ :: l, m => congrArg (_ :: ·) (map_append' f l m)122123theorem map_append_single {α β : Type} (f : α → β) (l : List α) (a : α) : (l ++ [a]).map f = l.map f ++ [f a] := map_append' f l [a]124125theorem nth_map_lt {α β : Type} (f : α → β) (d : α) (e : β) : ∀ (l : List α) (i : Nat), i < l.length → nth e (l.map f) i = f (nth d l i)126  | [], _, h => absurd h (Nat.not_lt_zero _)127  | _ :: _, 0, _ => rfl128  | _ :: l, i + 1, h => nth_map_lt f d e l i (Nat.lt_of_succ_lt_succ h)129130theorem nth_append_lt {α : Type} (d : α) : ∀ (l m : List α) (i : Nat), i < l.length → nth d (l ++ m) i = nth d l i131  | [], _, _, h => absurd h (Nat.not_lt_zero _)132  | _ :: _, _, 0, _ => rfl133  | _ :: l, m, i + 1, h => nth_append_lt d l m i (Nat.lt_of_succ_lt_succ h)134135theorem nth_append_len {α : Type} (d : α) : ∀ (l : List α) (a : α), nth d (l ++ [a]) l.length = a136  | [], _ => rfl137  | _ :: l, a => nth_append_len d l a138139theorem length_zipWith' {α β γ : Type} (f : α → β → γ) : ∀ (l : List α) (m : List β), l.length = m.length →140    (List.zipWith f l m).length = l.length141  | [], [], _ => rfl142  | [], _ :: _, h => absurd h (Nat.ne_of_lt (Nat.succ_pos _))143  | _ :: _, [], h => absurd h (Nat.ne_of_gt (Nat.succ_pos _))144  | _ :: l, _ :: m, h => congrArg (· + 1) (length_zipWith' f l m (Nat.succ.inj h))145146theorem nth_zipWith {α β γ : Type} (f : α → β → γ) (d : α) (e : β) (c : γ) : ∀ (l : List α) (m : List β) (i : Nat),147    i < l.length → i < m.length → nth c (List.zipWith f l m) i = f (nth d l i) (nth e m i)148  | [], _, _, h, _ => absurd h (Nat.not_lt_zero _)149  | _ :: _, [], _, _, h => absurd h (Nat.not_lt_zero _)150  | _ :: _, _ :: _, 0, _, _ => rfl151  | _ :: l, _ :: m, i + 1, h, h' => nth_zipWith f d e c l m i (Nat.lt_of_succ_lt_succ h) (Nat.lt_of_succ_lt_succ h')152153theorem ext_nth {α : Type} (d : α) : ∀ (l m : List α), l.length = m.length → (∀ i, i < l.length → nth d l i = nth d m i) → l = m154  | [], [], _, _ => rfl155  | [], _ :: _, h, _ => absurd h (Nat.ne_of_lt (Nat.succ_pos _))156  | _ :: _, [], h, _ => absurd h (Nat.ne_of_gt (Nat.succ_pos _))157  | a :: l, b :: m, h, e => by158    have hab : a = b := e 0 (Nat.succ_pos _)159    rw [hab, ext_nth d l m (Nat.succ.inj h) (fun i hi => e (i + 1) (Nat.succ_lt_succ hi))]160161theorem map_map' {α β γ : Type} (f : α → β) (g : β → γ) : ∀ l : List α, (l.map f).map g = l.map (fun x => g (f x))162  | [] => rfl163  | _ :: l => congrArg (_ :: ·) (map_map' f g l)164165theorem map_congr' {α β : Type} {f g : α → β} (h : ∀ x, f x = g x) : ∀ l : List α, l.map f = l.map g166  | [] => rfl167  | x :: l => by show f x :: _ = g x :: _; rw [h x, map_congr' h l]168169/-! ## The sign and the sums -/170171/-- `(−1)^i` in `K`. -/172def sgn : Nat → Ext p ν173  | 0 => 1174  | i + 1 => -(sgn i)175176theorem sgn_succ (i : Nat) : (sgn (i + 1) : Ext p ν) = -(sgn i) := rfl177theorem sgn_add_two (i : Nat) : (sgn (i + 2) : Ext p ν) = sgn i := Hermitian.neg_neg _178theorem sgn_add (i : Nat) : ∀ j : Nat, (sgn (i + j) : Ext p ν) = sgn i * sgn j179  | 0 => (Ext.mul_one _).symm180  | j + 1 => by181    show -(sgn (i + j)) = sgn i * -(sgn j)182    rw [sgn_add i j, Hermitian.mul_neg]183theorem sgn_mul_sgn (i : Nat) : (sgn i : Ext p ν) * sgn i = 1 := by184  induction i with185  | zero => exact Ext.one_mul (1 : Ext p ν)186  | succ i ih => show -(sgn i) * -(sgn i) = 1; rw [← Hermitian.neg_mul, ← Hermitian.mul_neg, Hermitian.neg_neg, ih]187188/-- `Σ_{j = i}^{i + k − 1} f j`. -/189def sumFrom (f : Nat → Ext p ν) : Nat → Nat → Ext p ν190  | 0, _ => 0191  | k + 1, i => f i + sumFrom f k (i + 1)192193theorem sumFrom_congr {f g : Nat → Ext p ν} : ∀ (k i : Nat), (∀ j, i ≤ j → j < i + k → f j = g j) →194    sumFrom f k i = sumFrom g k i195  | 0, _, _ => rfl196  | k + 1, i, h => by197    show f i + sumFrom f k (i + 1) = g i + sumFrom g k (i + 1)198    rw [h i (Nat.le_refl i) (Nat.lt_add_of_pos_right (Nat.succ_pos k)),199      sumFrom_congr k (i + 1) fun j hj hj' => h j (Nat.le_of_succ_le hj) (Nat.add_right_comm i 1 k ▸ hj')]200201theorem sumFrom_add (f g : Nat → Ext p ν) : ∀ (k i : Nat), sumFrom (fun j => f j + g j) k i = sumFrom f k i + sumFrom g k i202  | 0, _ => (add_zero _).symm203  | k + 1, i => by204    show f i + g i + sumFrom (fun j => f j + g j) k (i + 1) = f i + sumFrom f k (i + 1) + (g i + sumFrom g k (i + 1))205    rw [sumFrom_add f g k, add_add_add_comm]206207theorem sumFrom_smul (c : Ext p ν) (f : Nat → Ext p ν) : ∀ (k i : Nat), sumFrom (fun j => c * f j) k i = c * sumFrom f k i208  | 0, _ => (mul_zero c).symm209  | k + 1, i => by210    show c * f i + sumFrom (fun j => c * f j) k (i + 1) = c * (f i + sumFrom f k (i + 1))211    rw [sumFrom_smul c f k, mul_add]212213theorem sumFrom_neg (f : Nat → Ext p ν) : ∀ (k i : Nat), sumFrom (fun j => -(f j)) k i = -(sumFrom f k i)214  | 0, _ => Ext.ext Shell.neg_zero.symm Shell.neg_zero.symm215  | k + 1, i => by216    show -(f i) + sumFrom (fun j => -(f j)) k (i + 1) = -(f i + sumFrom f k (i + 1))217    rw [sumFrom_neg f k, neg_add_rev]218219theorem sumFrom_zero_fn : ∀ (k i : Nat), sumFrom (fun _ => (0 : Ext p ν)) k i = 0220  | 0, _ => rfl221  | k + 1, i => by show 0 + sumFrom (fun _ => (0 : Ext p ν)) k (i + 1) = 0; rw [sumFrom_zero_fn k, add_zero]222223/-- Splitting a sum after its first `m` terms. -/224theorem sumFrom_split (f : Nat → Ext p ν) : ∀ (m k i : Nat), sumFrom f m i + sumFrom f k (i + m) = sumFrom f (m + k) i225  | 0, k, i => by rw [Nat.zero_add]; exact Hermitian.zero_add _226  | m + 1, k, i => by227    rw [Nat.succ_add]228    show f i + sumFrom f m (i + 1) + sumFrom f k (i + (m + 1)) = f i + sumFrom f (m + k) (i + 1)229    rw [← sumFrom_split f m k (i + 1), Hermitian.add_assoc, Nat.add_right_comm]; rfl230231/-! ## The determinant by expansion along the first column -/232233/-- The minor at row `i`: the rows other than `i`, each without its head. -/234def minor (M : Mat p ν) (i : Nat) : Mat p ν := (removeAt M i).map List.tail235236/-- The term of row `i` in the expansion along the first column, `d` standing for the determinant of the minors. -/237def term (d : Mat p ν → Ext p ν) (M : Mat p ν) (i : Nat) : Ext p ν := sgn i * head (row M i) * d (minor M i)238239/-- The expansion with the number of rows as fuel. -/240def detF : Nat → Mat p ν → Ext p ν241  | 0, _ => 1242  | _ + 1, [] => 1243  | n + 1, M@(_ :: _) => sumFrom (term (detF n) M) M.length 0244245/-- The determinant of a square matrix (`1` for the empty matrix). -/246def det (M : Mat p ν) : Ext p ν := detF M.length M247248theorem length_minor (M : Mat p ν) (i : Nat) (h : i < M.length) : (minor M i).length + 1 = M.length := by249  unfold minor; rw [length_map]; exact length_removeAt M i h250251theorem length_minor_le {M : Mat p ν} {i n : Nat} (hM : M.length ≤ n + 1) (h : i < M.length) : (minor M i).length ≤ n :=252  Nat.le_of_succ_le_succ (show (minor M i).length + 1 ≤ n + 1 by rw [length_minor M i h]; exact hM)253254/-- The fuel does not matter once it covers the rows. -/255theorem detF_fuel_eq : ∀ (n m : Nat) (M : Mat p ν), M.length ≤ n → M.length ≤ m → detF n M = detF m M256  | 0, 0, _, _, _ => rfl257  | 0, _ + 1, [], _, _ => rfl258  | 0, _ + 1, _ :: _, h, _ => absurd h (Nat.not_succ_le_zero _)259  | _ + 1, 0, [], _, _ => rfl260  | _ + 1, 0, _ :: _, _, h => absurd h (Nat.not_succ_le_zero _)261  | _ + 1, _ + 1, [], _, _ => rfl262  | n + 1, m + 1, r :: rest, h, h' =>263    sumFrom_congr _ _ fun j _ hj => by264      have hj' : j < (r :: rest).length := Nat.lt_of_lt_of_eq hj (Nat.zero_add _)265      unfold term266      rw [detF_fuel_eq n m (minor (r :: rest) j) (length_minor_le h hj') (length_minor_le h' hj')]267268theorem detF_fuel (n : Nat) (M : Mat p ν) (h : M.length ≤ n) : detF n M = det M :=269  detF_fuel_eq n M.length M h (Nat.le_refl _)270271/-- The expansion along the first column. -/272theorem det_expand (M : Mat p ν) (h : 0 < M.length) : det M = sumFrom (term det M) M.length 0 := by273  match M, h with274  | r :: rest, _ =>275    show sumFrom (term (detF rest.length) (r :: rest)) (rest.length + 1) 0 = _276    exact sumFrom_congr _ _ fun j _ hj => by277      unfold term278      rw [detF_fuel rest.length (minor (r :: rest) j) (length_minor_le (Nat.le_refl _) (Nat.lt_of_lt_of_eq hj (Nat.zero_add _)))]279280theorem det_nil : det ([] : Mat p ν) = 1 := rfl281282theorem det_single (a : Ext p ν) : det [[a]] = a := by283  show 1 * a * 1 + 0 = a284  rw [Ext.one_mul, Ext.mul_one, add_zero]285286/-! ## Rows: replacement, addition, scaling -/287288/-- The sum and the scaling of rows. -/289def radd : List (Ext p ν) → List (Ext p ν) → List (Ext p ν)290  | [], _ => []291  | _ :: _, [] => []292  | a :: r, b :: s => (a + b) :: radd r s293def rsmul (c : Ext p ν) (r : List (Ext p ν)) : List (Ext p ν) := r.map (c * ·)294295theorem head_radd : ∀ (r s : List (Ext p ν)), r.length = s.length → head (radd r s) = head r + head s296  | [], [], _ => (add_zero _).symm297  | [], _ :: _, h => absurd h (Nat.ne_of_lt (Nat.succ_pos _))298  | _ :: _, [], h => absurd h (Nat.ne_of_gt (Nat.succ_pos _))299  | _ :: _, _ :: _, _ => rfl300301theorem tail_radd : ∀ (r s : List (Ext p ν)), (radd r s).tail = radd r.tail s.tail302  | [], _ => rfl303  | _ :: [], [] => rfl304  | _ :: _ :: _, [] => rfl305  | _ :: _, _ :: _ => rfl306307theorem length_radd : ∀ (r s : List (Ext p ν)), r.length = s.length → (radd r s).length = r.length308  | [], [], _ => rfl309  | [], _ :: _, h => absurd h (Nat.ne_of_lt (Nat.succ_pos _))310  | _ :: _, [], h => absurd h (Nat.ne_of_gt (Nat.succ_pos _))311  | _ :: r, _ :: s, h => congrArg (· + 1) (length_radd r s (Nat.succ.inj h))312313theorem length_tail {α : Type} : ∀ (l : List α), l.tail.length + 1 = l.length ∨ l = []314  | [] => Or.inr rfl315  | _ :: _ => Or.inl rfl316317theorem head_rsmul (c : Ext p ν) : ∀ r : List (Ext p ν), head (rsmul c r) = c * head r318  | [] => (mul_zero c).symm319  | _ :: _ => rfl320321theorem tail_rsmul (c : Ext p ν) : ∀ r : List (Ext p ν), (rsmul c r).tail = rsmul c r.tail322  | [] => rfl323  | _ :: _ => rfl324325theorem row_setAt_eq (M : Mat p ν) (i : Nat) (r : List (Ext p ν)) (h : i < M.length) : row (setAt M i r) i = r :=326  nth_setAt_eq [] M i r h327theorem row_setAt_ne (M : Mat p ν) (i j : Nat) (r : List (Ext p ν)) (h : i ≠ j) : row (setAt M i r) j = row M j :=328  nth_setAt_ne [] M i j r h329330theorem minor_setAt_gt (M : Mat p ν) (i j : Nat) (r : List (Ext p ν)) (h : i < j) :331    minor (setAt M i r) j = setAt (minor M j) i r.tail := by332  unfold minor; rw [removeAt_setAt_gt M i j r h, map_setAt]333theorem minor_setAt_lt (M : Mat p ν) (i j : Nat) (r : List (Ext p ν)) (h : j < i) :334    minor (setAt M i r) j = setAt (minor M j) (i - 1) r.tail := by335  unfold minor; rw [removeAt_setAt_lt M i j r h, map_setAt]336theorem minor_setAt_eq (M : Mat p ν) (i : Nat) (r : List (Ext p ν)) : minor (setAt M i r) i = minor M i := by337  unfold minor; rw [removeAt_setAt_eq]338339/-- The index of row `i` inside the minor at row `j`. -/340def shift (i j : Nat) : Nat := if j < i then i - 1 else i341342theorem minor_setAt (M : Mat p ν) (i j : Nat) (r : List (Ext p ν)) (h : i ≠ j) :343    minor (setAt M i r) j = setAt (minor M j) (shift i j) r.tail := by344  unfold shift345  match Nat.decLt j i with346  | .isTrue hji => rw [ite_eq_left hji]; exact minor_setAt_lt M i j r hji347  | .isFalse hji =>348    rw [ite_eq_right hji]349    exact minor_setAt_gt M i j r (Nat.lt_of_le_of_ne (Nat.le_of_not_lt hji) h)350351theorem shift_lt {i j n : Nat} (hi : i < n + 1) (hj : j < n + 1) (h : i ≠ j) : shift i j < n := by352  unfold shift353  match Nat.decLt j i with354  | .isTrue hji =>355    rw [ite_eq_left hji]356    exact Nat.lt_of_lt_of_le (Nat.sub_lt (Nat.lt_of_le_of_lt (Nat.zero_le j) hji) Nat.one_pos) (Nat.le_of_lt_succ hi)357  | .isFalse hji =>358    rw [ite_eq_right hji]359    exact Nat.lt_of_lt_of_le (Nat.lt_of_le_of_ne (Nat.le_of_not_lt hji) h) (Nat.le_of_lt_succ hj)360361/-- Linearity in a row: the sum. -/362theorem det_setAt_add : ∀ (n : Nat) (M : Mat p ν) (i : Nat) (r s : List (Ext p ν)), M.length = n + 1 → i < n + 1 →363    r.length = s.length → det (setAt M i (radd r s)) = det (setAt M i r) + det (setAt M i s)364  | n, M, i, r, s, hM, hi, hl => by365    have hlen : ∀ t, (setAt M i t).length = n + 1 := fun t => (length_setAt M i t).trans hM366    rw [det_expand _ (hlen _ ▸ Nat.succ_pos n), det_expand _ (hlen _ ▸ Nat.succ_pos n),367      det_expand _ (hlen _ ▸ Nat.succ_pos n), hlen, hlen, hlen, ← sumFrom_add]368    exact sumFrom_congr _ _ fun j _ hj => by369      have hj' : j < n + 1 := Nat.lt_of_lt_of_eq hj (Nat.zero_add _)370      unfold term371      match Nat.decEq i j with372      | .isTrue e =>373        subst e374        rw [row_setAt_eq _ _ _ (hM ▸ hi), row_setAt_eq _ _ _ (hM ▸ hi), row_setAt_eq _ _ _ (hM ▸ hi),375          minor_setAt_eq, minor_setAt_eq, minor_setAt_eq, head_radd r s hl, mul_add, add_mul]376      | .isFalse e =>377        rw [row_setAt_ne _ _ _ _ e, row_setAt_ne _ _ _ _ e, row_setAt_ne _ _ _ _ e,378          minor_setAt _ _ _ _ e, minor_setAt _ _ _ _ e, minor_setAt _ _ _ _ e, tail_radd]379        match n with380        | 0 => exact absurd (eq_zero_of_lt_one hi ▸ eq_zero_of_lt_one hj' ▸ e) (fun h => h rfl)381        | n + 1 =>382          have hjM : j < M.length := by rw [hM]; exact hj'383          rw [det_setAt_add n (minor M j) (shift i j) r.tail s.tail384            (Nat.succ.inj (show (minor M j).length + 1 = n + 1 + 1 by rw [length_minor M j hjM]; exact hM))385            (shift_lt hi hj' e) ?_, mul_add]386          match r, s, hl with387          | [], [], _ => rfl388          | _ :: _, _ :: _, h => exact Nat.succ.inj h389390theorem mul_left_comm (a b c : Ext p ν) : a * (b * c) = b * (a * c) := by391  rw [← Ext.mul_assoc, Ext.mul_comm a b, Ext.mul_assoc]392theorem add_left_comm (a b c : Ext p ν) : a + (b + c) = b + (a + c) := by393  rw [← Hermitian.add_assoc, Hermitian.add_comm a b, Hermitian.add_assoc]394395/-- Linearity in a row: the scaling. -/396theorem det_setAt_smul : ∀ (n : Nat) (M : Mat p ν) (i : Nat) (c : Ext p ν) (r : List (Ext p ν)), M.length = n + 1 →397    i < n + 1 → det (setAt M i (rsmul c r)) = c * det (setAt M i r)398  | n, M, i, c, r, hM, hi => by399    have hlen : ∀ t, (setAt M i t).length = n + 1 := fun t => (length_setAt M i t).trans hM400    rw [det_expand _ (hlen _ ▸ Nat.succ_pos n), det_expand _ (hlen _ ▸ Nat.succ_pos n), hlen, hlen, ← sumFrom_smul]401    exact sumFrom_congr _ _ fun j _ hj => by402      have hj' : j < n + 1 := Nat.lt_of_lt_of_eq hj (Nat.zero_add _)403      unfold term404      match Nat.decEq i j with405      | .isTrue e =>406        subst e407        rw [row_setAt_eq _ _ _ (hM ▸ hi), row_setAt_eq _ _ _ (hM ▸ hi), minor_setAt_eq, minor_setAt_eq, head_rsmul,408          mul_left_comm (sgn i) c, Ext.mul_assoc c]409      | .isFalse e =>410        rw [row_setAt_ne _ _ _ _ e, row_setAt_ne _ _ _ _ e, minor_setAt _ _ _ _ e, minor_setAt _ _ _ _ e, tail_rsmul]411        match n with412        | 0 => exact absurd (eq_zero_of_lt_one hi ▸ eq_zero_of_lt_one hj' ▸ e) (fun h => h rfl)413        | n + 1 =>414          have hjM : j < M.length := by rw [hM]; exact hj'415          rw [det_setAt_smul n (minor M j) (shift i j) c r.tail416            (Nat.succ.inj (show (minor M j).length + 1 = n + 1 + 1 by rw [length_minor M j hjM]; exact hM))417            (shift_lt hi hj' e), mul_left_comm _ c]418419/-! ## The adjacent swap and the vanishing on equal rows -/420421/-- The matrix with rows `i` and `i + 1` exchanged. -/422def swapAdj (M : Mat p ν) (i : Nat) : Mat p ν := setAt (setAt M i (row M (i + 1))) (i + 1) (row M i)423424theorem length_swapAdj (M : Mat p ν) (i : Nat) : (swapAdj M i).length = M.length := by425  unfold swapAdj; rw [length_setAt, length_setAt]426427theorem row_swapAdj_fst (M : Mat p ν) (i : Nat) (h : i + 1 < M.length) : row (swapAdj M i) i = row M (i + 1) := by428  unfold swapAdj429  rw [row_setAt_ne _ _ _ _ (Nat.ne_of_gt (Nat.lt_succ_self i)), row_setAt_eq _ _ _ (Nat.lt_of_succ_lt h)]430theorem row_swapAdj_snd (M : Mat p ν) (i : Nat) (h : i + 1 < M.length) : row (swapAdj M i) (i + 1) = row M i := by431  unfold swapAdj; rw [row_setAt_eq _ _ _ (by rw [length_setAt]; exact h)]432theorem row_swapAdj_other (M : Mat p ν) (i j : Nat) (h1 : j ≠ i) (h2 : j ≠ i + 1) : row (swapAdj M i) j = row M j := by433  unfold swapAdj; rw [row_setAt_ne _ _ _ _ (Ne.symm h2), row_setAt_ne _ _ _ _ (Ne.symm h1)]434435theorem nth_removeAt_lt {α : Type} (d : α) : ∀ (l : List α) (j k : Nat), k < j → nth d (removeAt l j) k = nth d l k436  | [], _, _, _ => rfl437  | _ :: _, 0, _, h => absurd h (Nat.not_lt_zero _)438  | _ :: _, _ + 1, 0, _ => rfl439  | _ :: l, j + 1, k + 1, h => nth_removeAt_lt d l j k (Nat.lt_of_succ_lt_succ h)440theorem nth_removeAt_ge {α : Type} (d : α) : ∀ (l : List α) (j k : Nat), j ≤ k → nth d (removeAt l j) k = nth d l (k + 1)441  | [], _, _, _ => rfl442  | _ :: _, 0, _, _ => rfl443  | _ :: _, _ + 1, 0, h => absurd h (Nat.not_succ_le_zero _)444  | _ :: l, j + 1, k + 1, h => nth_removeAt_ge d l j k (Nat.le_of_succ_le_succ h)445446theorem row_minor_lt (M : Mat p ν) (j k : Nat) (h : k < j) : row (minor M j) k = (row M k).tail := by447  show nth [] ((removeAt M j).map List.tail) k = (nth [] M k).tail448  rw [show nth [] ((removeAt M j).map List.tail) k = (nth [] (removeAt M j) k).tail from449    nth_map List.tail [] (removeAt M j) k, nth_removeAt_lt _ _ _ _ h]450theorem row_minor_ge (M : Mat p ν) (j k : Nat) (h : j ≤ k) : row (minor M j) k = (row M (k + 1)).tail := by451  show nth [] ((removeAt M j).map List.tail) k = (nth [] M (k + 1)).tail452  rw [show nth [] ((removeAt M j).map List.tail) k = (nth [] (removeAt M j) k).tail from453    nth_map List.tail [] (removeAt M j) k, nth_removeAt_ge _ _ _ _ h]454455/-- Removing entry `i` and writing it back at `i` removes entry `i + 1`. -/456theorem removeAt_succ_eq {α : Type} (d : α) : ∀ (l : List α) (i : Nat), i + 1 < l.length →457    setAt (removeAt l i) i (nth d l i) = removeAt l (i + 1)458  | [], _, h => absurd h (Nat.not_lt_zero _)459  | _ :: [], 0, h => absurd (Nat.lt_of_succ_lt_succ h) (Nat.not_lt_zero _)460  | _ :: _ :: _, 0, _ => rfl461  | _ :: l, i + 1, h => congrArg (_ :: ·) (removeAt_succ_eq d l i (Nat.lt_of_succ_lt_succ h))462463/-- The minor at `i` of the swap at `i` is the minor at `i + 1`, and conversely. -/464theorem minor_swapAdj_fst (M : Mat p ν) (i : Nat) (h : i + 1 < M.length) : minor (swapAdj M i) i = minor M (i + 1) := by465  unfold swapAdj466  rw [minor_setAt_lt _ _ _ _ (Nat.lt_succ_self i), minor_setAt_eq]467  show setAt (minor M i) i (row M i).tail = minor M (i + 1)468  unfold minor469  rw [← map_setAt]470  exact congrArg (List.map List.tail) (removeAt_succ_eq [] M i h)471472theorem setAt_removeAt_succ {α : Type} (d : α) : ∀ (l : List α) (i : Nat), i + 1 < l.length →473    setAt (removeAt l (i + 1)) i (nth d l (i + 1)) = removeAt l i474  | [], _, h => absurd h (Nat.not_lt_zero _)475  | _ :: [], 0, h => absurd (Nat.lt_of_succ_lt_succ h) (Nat.not_lt_zero _)476  | _ :: _ :: _, 0, _ => rfl477  | _ :: l, i + 1, h => congrArg (_ :: ·) (setAt_removeAt_succ d l i (Nat.lt_of_succ_lt_succ h))478479theorem minor_swapAdj_snd (M : Mat p ν) (i : Nat) (h : i + 1 < M.length) : minor (swapAdj M i) (i + 1) = minor M i := by480  unfold swapAdj481  rw [minor_setAt_eq, minor_setAt_gt _ _ _ _ (Nat.lt_succ_self i)]482  show setAt (minor M (i + 1)) i (row M (i + 1)).tail = minor M i483  unfold minor484  rw [← map_setAt]485  exact congrArg (List.map List.tail) (setAt_removeAt_succ [] M i h)486487theorem shift_succ (i j : Nat) (h1 : j ≠ i) (h2 : j ≠ i + 1) : shift (i + 1) j = shift i j + 1 := by488  unfold shift489  match Nat.decLt j i with490  | .isTrue hji =>491    rw [ite_eq_left (Nat.lt_succ_of_lt hji), ite_eq_left hji]492    match i, hji with493    | i' + 1, _ => rfl494  | .isFalse hji =>495    rw [ite_eq_right hji, ite_eq_right]496    intro hj; exact h1 (Nat.le_antisymm (Nat.le_of_lt_succ hj) (Nat.le_of_not_lt hji))497498theorem minor_swapAdj_other (M : Mat p ν) (i j : Nat) (h1 : j ≠ i) (h2 : j ≠ i + 1) :499    minor (swapAdj M i) j = swapAdj (minor M j) (shift i j) := by500  unfold swapAdj501  rw [minor_setAt _ _ _ _ (Ne.symm h2), minor_setAt _ _ _ _ (Ne.symm h1), shift_succ i j h1 h2]502  unfold shift503  match Nat.decLt j i with504  | .isTrue hji =>505    rw [ite_eq_left hji]506    match i, hji with507    | i' + 1, hji' =>508      show setAt (setAt (minor M j) i' (row M (i' + 1 + 1)).tail) (i' + 1) (row M (i' + 1)).tail =509        setAt (setAt (minor M j) i' (row (minor M j) (i' + 1))) (i' + 1) (row (minor M j) i')510      rw [← row_minor_ge M j (i' + 1) (Nat.le_of_lt hji'), ← row_minor_ge M j i' (Nat.le_of_lt_succ hji')]511  | .isFalse hji =>512    rw [ite_eq_right hji]513    have hij : i + 1 < j := Nat.lt_of_le_of_ne (Nat.lt_of_le_of_ne (Nat.le_of_not_lt hji) (Ne.symm h1)) (Ne.symm h2)514    rw [← row_minor_lt M j (i + 1) hij, ← row_minor_lt M j i (Nat.lt_of_succ_lt hij)]515516/-- The transposition of `i` and `i + 1`. -/517def tr (i j : Nat) : Nat := if j = i then i + 1 else if j = i + 1 then i else j518519theorem tr_fst (i : Nat) : tr i i = i + 1 := by unfold tr; rw [ite_eq_left rfl]520theorem tr_snd (i : Nat) : tr i (i + 1) = i := by521  unfold tr; rw [ite_eq_right (Nat.ne_of_gt (Nat.lt_succ_self i)), ite_eq_left rfl]522theorem tr_other (i j : Nat) (h1 : j ≠ i) (h2 : j ≠ i + 1) : tr i j = j := by523  unfold tr; rw [ite_eq_right h1, ite_eq_right h2]524525/-- A sum is unchanged by exchanging two adjacent summands. -/526theorem sumFrom_tr (f : Nat → Ext p ν) (i m : Nat) :527    sumFrom (fun j => f (tr i j)) (i + (m + 2)) 0 = sumFrom f (i + (m + 2)) 0 := by528    rw [← sumFrom_split _ i (m + 2) 0, ← sumFrom_split f i (m + 2) 0, Nat.zero_add]529    rw [sumFrom_congr i 0 (fun j _ hj => by530      rw [tr_other i j (Nat.ne_of_lt (Nat.lt_of_lt_of_eq hj (Nat.zero_add i)))531        (Nat.ne_of_lt (Nat.lt_succ_of_lt (Nat.lt_of_lt_of_eq hj (Nat.zero_add i))))])]532    show sumFrom f i 0 + (f (tr i i) + (f (tr i (i + 1)) + sumFrom (fun j => f (tr i j)) m (i + 2))) =533      sumFrom f i 0 + (f i + (f (i + 1) + sumFrom f m (i + 2)))534    rw [tr_fst, tr_snd, sumFrom_congr m (i + 2) (fun j hj _ => by535      rw [tr_other i j (Nat.ne_of_gt (Nat.lt_of_lt_of_le (Nat.lt_succ_of_lt (Nat.lt_succ_self i)) hj))536        (Nat.ne_of_gt (Nat.lt_of_lt_of_le (Nat.lt_succ_self (i + 1)) hj))]), add_left_comm (f (i + 1)) (f i)]537538/-- The adjacent swap negates the determinant. -/539theorem det_swapAdj : ∀ (n : Nat) (M : Mat p ν) (i : Nat), M.length = n + 2 → i + 1 < n + 2 → det (swapAdj M i) = -(det M)540  | n, M, i, hM, hi => by541    have hlen : (swapAdj M i).length = n + 2 := (length_swapAdj M i).trans hM542    have hiM : i + 1 < M.length := hM ▸ hi543    rw [det_expand _ (hlen ▸ Nat.succ_pos _), det_expand _ (hM ▸ Nat.succ_pos _), hlen, hM, ← sumFrom_neg]544    have hk : n + 2 = i + (n - i + 2) := by545      rw [← Nat.add_assoc, FRC.Nat.add_sub_of_le (Nat.le_of_lt_succ (Nat.lt_of_succ_lt_succ hi))]546    rw [hk, ← sumFrom_tr (fun j => -(term det M j)) i (n - i)]547    exact sumFrom_congr _ _ fun j _ hj => by548      have hj' : j < n + 2 := Nat.lt_of_lt_of_eq hj (by rw [Nat.zero_add]; exact hk.symm)549      unfold term550      match Nat.decEq j i with551      | .isTrue e =>552        subst e553        rw [tr_fst, row_swapAdj_fst M j hiM, minor_swapAdj_fst M j hiM, sgn_succ, ← Hermitian.neg_mul, ← Hermitian.neg_mul,554          Hermitian.neg_neg]555      | .isFalse e1 =>556        match Nat.decEq j (i + 1) with557        | .isTrue e =>558          subst e559          rw [tr_snd, row_swapAdj_snd M i hiM, minor_swapAdj_snd M i hiM, sgn_succ, ← Hermitian.neg_mul, ← Hermitian.neg_mul]560        | .isFalse e2 =>561          rw [tr_other i j e1 e2, row_swapAdj_other M i j e1 e2, minor_swapAdj_other M i j e1 e2]562          match n with563          | 0 =>564            match i, j, hi, hj' with565            | 0, 0, _, _ => exact absurd rfl e1566            | 0, 1, _, _ => exact absurd rfl e2567            | 0, _ + 2, _, hj => exact absurd (Nat.lt_of_succ_lt_succ (Nat.lt_of_succ_lt_succ hj)) (Nat.not_lt_zero _)568            | _ + 1, _, hi, _ => exact absurd (Nat.lt_of_succ_lt_succ (Nat.lt_of_succ_lt_succ hi)) (Nat.not_lt_zero _)569          | n + 1 =>570            have hjM : j < M.length := by rw [hM]; exact hj'571            rw [det_swapAdj n (minor M j) (shift i j)572              (Nat.succ.inj (show (minor M j).length + 1 = n + 2 + 1 by rw [length_minor M j hjM]; exact hM))573              (shift_succ i j e1 e2 ▸ shift_lt hi hj' (Ne.symm e2)), Hermitian.mul_neg]574575/-! ## Two equal rows -/576577theorem removeAt_eq_of_eq {α : Type} (d : α) : ∀ (l : List α) (i : Nat), i + 1 < l.length → nth d l i = nth d l (i + 1) →578    removeAt l i = removeAt l (i + 1)579  | [], _, h, _ => absurd h (Nat.not_lt_zero _)580  | _ :: [], 0, h, _ => absurd (Nat.lt_of_succ_lt_succ h) (Nat.not_lt_zero _)581  | a :: b :: l, 0, _, e => by582    show b :: l = a :: l583    exact congrArg (· :: l) (show a = b from e).symm584  | _ :: l, i + 1, h, e => congrArg (_ :: ·) (removeAt_eq_of_eq d l i (Nat.lt_of_succ_lt_succ h) e)585586theorem minor_eq_of_adj_eq (M : Mat p ν) (i : Nat) (h : i + 1 < M.length) (e : row M i = row M (i + 1)) :587    minor M i = minor M (i + 1) := by588  unfold minor; rw [removeAt_eq_of_eq [] M i h e]589590theorem term_eq_zero_of_minor {d : Mat p ν → Ext p ν} {M : Mat p ν} {j : Nat} (h : d (minor M j) = 0) : term d M j = 0 := by591  unfold term; rw [h, mul_zero]592593theorem neg_eq_zero {x : Ext p ν} (h : -x = 0) : x = 0 := by594  rw [← Hermitian.neg_neg x, h]; exact Ext.ext Shell.neg_zero Shell.neg_zero595596/-- Two equal adjacent rows: the determinant vanishes. -/597theorem det_adj_eq_zero : ∀ (n : Nat) (M : Mat p ν) (i : Nat), M.length = n + 2 → i + 1 < n + 2 → row M i = row M (i + 1) →598    det M = 0599  | n, M, i, hM, hi, e => by600    have hiM : i + 1 < M.length := hM ▸ hi601    rw [det_expand _ (hM ▸ Nat.succ_pos _), hM]602    have hk : n + 2 = i + (n - i + 2) := by603      rw [← Nat.add_assoc, FRC.Nat.add_sub_of_le (Nat.le_of_lt_succ (Nat.lt_of_succ_lt_succ hi))]604    rw [hk, ← sumFrom_split _ i (n - i + 2) 0, Nat.zero_add]605    show sumFrom (term det M) i 0 + (term det M i + (term det M (i + 1) + sumFrom (term det M) (n - i) (i + 2))) = 0606    -- the two terms of the equal rows cancel607    have h2 : term det M i + term det M (i + 1) = 0 := by608      unfold term609      rw [minor_eq_of_adj_eq M i hiM e, ← e, sgn_succ, ← Hermitian.neg_mul, ← Hermitian.neg_mul, add_neg]610    -- the other terms vanish by induction611    have hlow : sumFrom (term det M) i 0 = 0 := by612      rw [← sumFrom_zero_fn i 0]613      exact sumFrom_congr _ _ fun j _ hj => by614        have hji : j < i := Nat.lt_of_lt_of_eq hj (Nat.zero_add i)615        apply term_eq_zero_of_minor616        match n, hi with617        | 0, hi => exact absurd (Nat.lt_of_lt_of_le hji (Nat.le_of_lt_succ (Nat.lt_of_succ_lt_succ hi))) (Nat.not_lt_zero _)618        | n + 1, hi =>619          have hjM : j < M.length := by rw [hM]; exact Nat.lt_of_lt_of_le hji (Nat.le_of_lt (Nat.lt_of_succ_lt hi))620          refine det_adj_eq_zero n (minor M j) (i - 1)621            (Nat.succ.inj (show (minor M j).length + 1 = n + 2 + 1 by rw [length_minor M j hjM]; exact hM)) ?_ ?_622          · match i, hji, hi with623            | i' + 1, _, hi => exact Nat.lt_of_succ_lt_succ hi624          · match i, hji with625            | i' + 1, hji =>626              show row (minor M j) i' = row (minor M j) (i' + 1)627              rw [row_minor_ge M j i' (Nat.le_of_lt_succ hji), row_minor_ge M j (i' + 1) (Nat.le_of_lt hji), e]628    have hhigh : sumFrom (term det M) (n - i) (i + 2) = 0 := by629      rw [← sumFrom_zero_fn (n - i) (i + 2)]630      exact sumFrom_congr _ _ fun j hj hj' => by631        apply term_eq_zero_of_minor632        have hjn : j < n + 2 := by633          have := FRC.Nat.add_sub_of_le (Nat.le_of_lt_succ (Nat.lt_of_succ_lt_succ hi))634          rw [Nat.add_right_comm] at hj'; rw [this] at hj'; exact hj'635        match n, i, hi, hj, hj' with636        | 0, 0, _, hj, hj' => exact absurd (Nat.lt_of_le_of_lt hj hj') (Nat.lt_irrefl _)637        | 0, _ + 1, hi, _, _ => exact absurd (Nat.lt_of_succ_lt_succ (Nat.lt_of_succ_lt_succ hi)) (Nat.not_lt_zero _)638        | n + 1, i, hi, hj, _ =>639          have hjM : j < M.length := by rw [hM]; exact hjn640          refine det_adj_eq_zero n (minor M j) i641            (Nat.succ.inj (show (minor M j).length + 1 = n + 2 + 1 by rw [length_minor M j hjM]; exact hM))642            (Nat.lt_of_succ_lt_succ (Nat.lt_of_le_of_lt hj hjn)) ?_643          rw [row_minor_lt M j i (Nat.lt_of_succ_lt (Nat.lt_of_succ_le hj)),644            row_minor_lt M j (i + 1) (Nat.lt_of_succ_le hj), e]645    rw [hlow, hhigh, add_zero, zero_add, h2]646647theorem length_form_two {α : Type} {l : List α} (h : 2 ≤ l.length) : l.length = l.length - 2 + 2 := (FRC.Nat.sub_add_cancel h).symm648theorem length_form_one {α : Type} {l : List α} (h : 1 ≤ l.length) : l.length = l.length - 1 + 1 := (FRC.Nat.sub_add_cancel h).symm649650/-- Two equal rows at `i` and `i + d + 1`: the determinant vanishes (the lower row brought up by adjacent swaps). -/651theorem det_rows_eq_zero : ∀ (d : Nat) (M : Mat p ν) (i : Nat), i + d + 1 < M.length → row M i = row M (i + d + 1) → det M = 0652  | 0, M, i, h, e =>653    have h2 : 2 ≤ M.length := Nat.le_trans (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le i))) h654    det_adj_eq_zero (M.length - 2) M i (length_form_two h2) (length_form_two h2 ▸ h) e655  | d + 1, M, i, h, e => by656    have h2 : 2 ≤ M.length := Nat.le_trans (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _))) h657    have hne1 : i ≠ i + d + 1 := Nat.ne_of_lt (Nat.lt_succ_of_le (Nat.le_add_right i d))658    have hne2 : i ≠ i + d + 1 + 1 := Nat.ne_of_lt (Nat.lt_succ_of_lt (Nat.lt_succ_of_le (Nat.le_add_right i d)))659    have hrec := det_rows_eq_zero d (swapAdj M (i + d + 1)) i660      (by rw [length_swapAdj]; exact Nat.lt_of_succ_lt h)661      (by rw [row_swapAdj_other M (i + d + 1) i hne1 hne2, row_swapAdj_fst M (i + d + 1) h]; exact e)662    rw [det_swapAdj (M.length - 2) M (i + d + 1) (length_form_two h2) (length_form_two h2 ▸ h)] at hrec663    exact neg_eq_zero hrec664665/-- Two equal rows at any two positions. -/666theorem det_rows_eq_zero' (M : Mat p ν) (i k : Nat) (hik : i ≠ k) (hi : i < M.length) (hk : k < M.length)667    (e : row M i = row M k) : det M = 0 := by668  match Nat.lt_or_ge i k with669  | .inl hlt =>670    have hd : i + (k - i - 1) + 1 = k := by671      rw [Nat.add_assoc, FRC.Nat.sub_add_cancel (sub_pos_of_lt' hlt), FRC.Nat.add_sub_of_le (Nat.le_of_lt hlt)]672    exact det_rows_eq_zero (k - i - 1) M i (by rw [hd]; exact hk) (by rw [hd]; exact e)673  | .inr hge =>674    have hlt : k < i := Nat.lt_of_le_of_ne hge (Ne.symm hik)675    have hd : k + (i - k - 1) + 1 = i := by676      rw [Nat.add_assoc, FRC.Nat.sub_add_cancel (sub_pos_of_lt' hlt), FRC.Nat.add_sub_of_le (Nat.le_of_lt hlt)]677    exact det_rows_eq_zero (i - k - 1) M k (by rw [hd]; exact hi) (by rw [hd]; exact e.symm)678679/-! ## Row operations and square matrices -/680681/-- A square matrix: every row as long as the list of rows. -/682def Square (M : Mat p ν) : Prop := ∀ i, i < M.length → (row M i).length = M.length683684theorem setAt_self {α : Type} (d : α) : ∀ (l : List α) (i : Nat), i < l.length → setAt l i (nth d l i) = l685  | [], _, h => absurd h (Nat.not_lt_zero _)686  | _ :: _, 0, _ => rfl687  | _ :: l, i + 1, h => congrArg (_ :: ·) (setAt_self d l i (Nat.lt_of_succ_lt_succ h))688689theorem length_rsmul (c : Ext p ν) (r : List (Ext p ν)) : (rsmul c r).length = r.length := length_map _ r690theorem setAt_row_self (M : Mat p ν) (i : Nat) (h : i < M.length) : setAt M i (row M i) = M := setAt_self [] M i h691692/-- Adding a multiple of row `k` to row `i` leaves the determinant unchanged. -/693theorem det_addRow (M : Mat p ν) (hS : Square M) (i k : Nat) (hik : i ≠ k) (hi : i < M.length) (hk : k < M.length)694    (c : Ext p ν) : det (setAt M i (radd (row M i) (rsmul c (row M k)))) = det M := by695  have hn : M.length = M.length - 1 + 1 := length_form_one (Nat.lt_of_le_of_lt (Nat.zero_le i) hi)696  have hi' : i < M.length - 1 + 1 := by rw [← hn]; exact hi697  rw [det_setAt_add (M.length - 1) M i _ _ hn hi' (by rw [length_rsmul]; exact (hS i hi).trans (hS k hk).symm),698    det_setAt_smul (M.length - 1) M i c _ hn hi', setAt_row_self M i hi,699    det_rows_eq_zero' (setAt M i (row M k)) i k hik (by rw [length_setAt]; exact hi) (by rw [length_setAt]; exact hk)700      (by rw [row_setAt_eq _ _ _ hi, row_setAt_ne _ _ _ _ hik]), mul_zero, add_zero]701702end FRC.Dirac.Det703