m : Type u
n✝ : Type v
α : Type w
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) α
i j : Fin (Nat.succ n)
⊢ ∑ x : Fin (Nat.succ n), (-1) ^ (↑j + ↑x) * Pi.single i 1 x * det (submatrix A ↑(Fin.succAbove j) ↑(Fin.succAbove x)) =
    (-1) ^ (↑j + ↑i) * det (submatrix A ↑(Fin.succAbove j) ↑(Fin.succAbove i))
m : Type u
n✝ : Type v
α : Type w
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) α
i j : Fin (Nat.succ n)
⊢ adjugate A i j = (-1) ^ (↑j + ↑i) * det (submatrix A ↑(Fin.succAbove j) ↑(Fin.succAbove i))
simp_rw [adjugate_apply, det_succ_row _ j, updateRow_self, submatrix_updateRow_succAbove]
m : Type u
n✝ : Type v
α : Type w
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) α
i j h : Fin (Nat.succ n)
hjk : h ≠ i
⊢ (-1) ^ (↑j + ↑h) * Pi.single i 1 h * det (submatrix A ↑(Fin.succAbove j) ↑(Fin.succAbove h)) = 0
m : Type u
n✝ : Type v
α : Type w
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) α
i j : Fin (Nat.succ n)
⊢ ∑ x : Fin (Nat.succ n), (-1) ^ (↑j + ↑x) * Pi.single i 1 x * det (submatrix A ↑(Fin.succAbove j) ↑(Fin.succAbove x)) =
    (-1) ^ (↑j + ↑i) * det (submatrix A ↑(Fin.succAbove j) ↑(Fin.succAbove i))
rw [Fintype.sum_eq_single i fun h hjk => ?_, Pi.single_eq_same, mul_one]
no goals
m : Type u
n✝ : Type v
α : Type w
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) α
i j h : Fin (Nat.succ n)
hjk : h ≠ i
⊢ (-1) ^ (↑j + ↑h) * Pi.single i 1 h * det (submatrix A ↑(Fin.succAbove j) ↑(Fin.succAbove h)) = 0
rw [Pi.single_eq_of_ne hjk, MulZeroClass.mul_zero, MulZeroClass.zero_mul]