m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
⊢ det A = ∑ j : n, A i j * adjugate A j i
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
⊢ det A = ∑ j : n, A i j * adjugate A j i
haveI : Nonempty n := ⟨i⟩
case intro
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
⊢ det A = ∑ j : n, A i j * adjugate A j i
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
⊢ det A = ∑ j : n, A i j * adjugate A j i
obtain ⟨n', hn'⟩ := Nat.exists_eq_succ_of_ne_zero (Fintype.card_ne_zero : Fintype.card n ≠ 0)
case intro.mk
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
⊢ det A = ∑ j : n, A i j * adjugate A j i
case intro
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
⊢ det A = ∑ j : n, A i j * adjugate A j i
obtain ⟨e⟩ := Fintype.truncEquivFinOfCardEq hn'
case intro.mk
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
A' : (fun x => Matrix (Fin (Nat.succ n')) (Fin (Nat.succ n')) α) A := ↑(reindex e e) A
⊢ det A = ∑ j : n, A i j * adjugate A j i
case intro.mk
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
⊢ det A = ∑ j : n, A i j * adjugate A j i
let A' := reindex e e A
case intro.mk
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
A' : (fun x => Matrix (Fin (Nat.succ n')) (Fin (Nat.succ n')) α) A := ↑(reindex e e) A
⊢ det A' = ∑ j : Fin (Nat.succ n'), A' (↑e i) j * adjugate A' j (↑e i)
case intro.mk
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
A' : (fun x => Matrix (Fin (Nat.succ n')) (Fin (Nat.succ n')) α) A := ↑(reindex e e) A
⊢ det A = ∑ j : n, A i j * adjugate A j i
suffices det A' = ∑ j : Fin n'.succ, A' (e i) j * adjugate A' j (e i) by
  simp_rw [det_reindex_self, adjugate_reindex, reindex_apply, submatrix_apply, ← e.sum_comp,
    Equiv.symm_apply_apply] at this
  exact this
case intro.mk
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
A' : (fun x => Matrix (Fin (Nat.succ n')) (Fin (Nat.succ n')) α) A := ↑(reindex e e) A
⊢ ∑ j : Fin (Nat.succ n'),
      (-1) ^ (↑(↑e i) + ↑j) * A' (↑e i) j * det (submatrix A' ↑(Fin.succAbove (↑e i)) ↑(Fin.succAbove j)) =
    ∑ j : Fin (Nat.succ n'), A' (↑e i) j * adjugate A' j (↑e i)
case intro.mk
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
A' : (fun x => Matrix (Fin (Nat.succ n')) (Fin (Nat.succ n')) α) A := ↑(reindex e e) A
⊢ det A' = ∑ j : Fin (Nat.succ n'), A' (↑e i) j * adjugate A' j (↑e i)
rw [det_succ_row A' (e i)]
no goals
case intro.mk
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
A' : (fun x => Matrix (Fin (Nat.succ n')) (Fin (Nat.succ n')) α) A := ↑(reindex e e) A
⊢ ∑ j : Fin (Nat.succ n'),
      (-1) ^ (↑(↑e i) + ↑j) * A' (↑e i) j * det (submatrix A' ↑(Fin.succAbove (↑e i)) ↑(Fin.succAbove j)) =
    ∑ j : Fin (Nat.succ n'), A' (↑e i) j * adjugate A' j (↑e i)
simp_rw [mul_assoc, mul_left_comm _ (A' _ _), ← adjugate_fin_succ_eq_det_submatrix]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this✝ : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
A' : (fun x => Matrix (Fin (Nat.succ n')) (Fin (Nat.succ n')) α) A := ↑(reindex e e) A
this : det A = ∑ x : n, A i x * adjugate A x i
⊢ det A = ∑ j : n, A i j * adjugate A j i
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this✝ : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
A' : (fun x => Matrix (Fin (Nat.succ n')) (Fin (Nat.succ n')) α) A := ↑(reindex e e) A
this : det A' = ∑ j : Fin (Nat.succ n'), A' (↑e i) j * adjugate A' j (↑e i)
⊢ det A = ∑ j : n, A i j * adjugate A j i
simp_rw [det_reindex_self, adjugate_reindex, reindex_apply, submatrix_apply, ← e.sum_comp,
  Equiv.symm_apply_apply] at this
no goals
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this✝ : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
A' : (fun x => Matrix (Fin (Nat.succ n')) (Fin (Nat.succ n')) α) A := ↑(reindex e e) A
this : det A = ∑ x : n, A i x * adjugate A x i
⊢ det A = ∑ j : n, A i j * adjugate A j i
exact this