m : Type ?u.2570289
n✝ : Type ?u.2570292
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
j : Fin (Nat.succ n)
⊢ ∑ j_1 : Fin (Nat.succ n), (-1) ^ (↑j + ↑j_1) * Aᵀ j j_1 * det (submatrix Aᵀ ↑(Fin.succAbove j) ↑(Fin.succAbove j_1)) =
    ∑ i : Fin (Nat.succ n), (-1) ^ (↑i + ↑j) * A i j * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove j))
m : Type ?u.2570289
n✝ : Type ?u.2570292
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
j : Fin (Nat.succ n)
⊢ det A = ∑ i : Fin (Nat.succ n), (-1) ^ (↑i + ↑j) * A i j * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove j))
rw [← det_transpose, det_succ_row _ j]
m : Type ?u.2570289
n✝ : Type ?u.2570292
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
j i : Fin (Nat.succ n)
x✝ : i ∈ univ
⊢ (-1) ^ (↑j + ↑i) * Aᵀ j i * det (submatrix Aᵀ ↑(Fin.succAbove j) ↑(Fin.succAbove i)) =
    (-1) ^ (↑i + ↑j) * A i j * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove j))
m : Type ?u.2570289
n✝ : Type ?u.2570292
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
j : Fin (Nat.succ n)
⊢ ∑ j_1 : Fin (Nat.succ n), (-1) ^ (↑j + ↑j_1) * Aᵀ j j_1 * det (submatrix Aᵀ ↑(Fin.succAbove j) ↑(Fin.succAbove j_1)) =
    ∑ i : Fin (Nat.succ n), (-1) ^ (↑i + ↑j) * A i j * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove j))
refine' Finset.sum_congr rfl fun i _ => _
no goals
m : Type ?u.2570289
n✝ : Type ?u.2570292
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
j i : Fin (Nat.succ n)
x✝ : i ∈ univ
⊢ (-1) ^ (↑j + ↑i) * Aᵀ j i * det (submatrix Aᵀ ↑(Fin.succAbove j) ↑(Fin.succAbove i)) =
    (-1) ^ (↑i + ↑j) * A i j * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove j))
rw [add_comm, ← det_transpose, transpose_apply, transpose_submatrix, transpose_transpose]