m : Type ?u.2165579
n✝ : Type ?u.2165582
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
⊢ ∑ i : Fin (Nat.succ n), (-1) ^ ↑i * Aᵀ i 0 * det (submatrix Aᵀ (↑(Fin.succAbove i)) Fin.succ) =
    ∑ j : Fin (Nat.succ n), (-1) ^ ↑j * A 0 j * det (submatrix A Fin.succ ↑(Fin.succAbove j))
m : Type ?u.2165579
n✝ : Type ?u.2165582
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
⊢ det A = ∑ j : Fin (Nat.succ n), (-1) ^ ↑j * A 0 j * det (submatrix A Fin.succ ↑(Fin.succAbove j))
rw [← det_transpose A, det_succ_column_zero]
m : Type ?u.2165579
n✝ : Type ?u.2165582
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
x✝ : i ∈ univ
⊢ (-1) ^ ↑i * Aᵀ i 0 * det (submatrix Aᵀ (↑(Fin.succAbove i)) Fin.succ) =
    (-1) ^ ↑i * A 0 i * det (submatrix A Fin.succ ↑(Fin.succAbove i))
m : Type ?u.2165579
n✝ : Type ?u.2165582
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
⊢ ∑ i : Fin (Nat.succ n), (-1) ^ ↑i * Aᵀ i 0 * det (submatrix Aᵀ (↑(Fin.succAbove i)) Fin.succ) =
    ∑ j : Fin (Nat.succ n), (-1) ^ ↑j * A 0 j * det (submatrix A Fin.succ ↑(Fin.succAbove j))
refine' Finset.sum_congr rfl fun i _ => _
m : Type ?u.2165579
n✝ : Type ?u.2165582
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
x✝ : i ∈ univ
⊢ (-1) ^ ↑i * Aᵀ i 0 * det (submatrix Aᵀ (↑(Fin.succAbove i)) Fin.succ)ᵀ =
    (-1) ^ ↑i * A 0 i * det (submatrix A Fin.succ ↑(Fin.succAbove i))
m : Type ?u.2165579
n✝ : Type ?u.2165582
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
x✝ : i ∈ univ
⊢ (-1) ^ ↑i * Aᵀ i 0 * det (submatrix Aᵀ (↑(Fin.succAbove i)) Fin.succ) =
    (-1) ^ ↑i * A 0 i * det (submatrix A Fin.succ ↑(Fin.succAbove i))
rw [← det_transpose]
no goals
m : Type ?u.2165579
n✝ : Type ?u.2165582
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
x✝ : i ∈ univ
⊢ (-1) ^ ↑i * Aᵀ i 0 * det (submatrix Aᵀ (↑(Fin.succAbove i)) Fin.succ)ᵀ =
    (-1) ^ ↑i * A 0 i * det (submatrix A Fin.succ ↑(Fin.succAbove i))
simp only [transpose_apply, transpose_submatrix, transpose_transpose]