case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ adjugate (submatrix A ↑e ↑e) i j = submatrix (adjugate A) (↑e) (↑e) i j
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
⊢ adjugate (submatrix A ↑e ↑e) = submatrix (adjugate A) ↑e ↑e
ext (i j)
case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ det (submatrix (updateRow A (↑e j) fun j => Pi.single i 1 (↑e.symm j)) ↑e ↑e) =
    det (submatrix (updateRow A (↑e j) (Pi.single (↑e i) 1)) ↑e ↑e)
case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ adjugate (submatrix A ↑e ↑e) i j = submatrix (adjugate A) (↑e) (↑e) i j
rw [adjugate_apply, submatrix_apply, adjugate_apply, ← det_submatrix_equiv_self e,
  updateRow_submatrix_equiv]
case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ (fun j => Pi.single i 1 (↑e.symm j)) = Pi.single (↑e i) 1
case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ det (submatrix (updateRow A (↑e j) fun j => Pi.single i 1 (↑e.symm j)) ↑e ↑e) =
    det (submatrix (updateRow A (↑e j) (Pi.single (↑e i) 1)) ↑e ↑e)
suffices (fun j => Pi.single i 1 (e.symm j)) = Pi.single (e i) 1 by
  erw [this]
no goals
case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ (fun j => Pi.single i 1 (↑e.symm j)) = Pi.single (↑e i) 1
exact Function.update_comp_equiv _ e.symm _ _
no goals
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
this : (fun j => Pi.single i 1 (↑e.symm j)) = Pi.single (↑e i) 1
⊢ det (submatrix (updateRow A (↑e j) fun j => Pi.single i 1 (↑e.symm j)) ↑e ↑e) =
    det (submatrix (updateRow A (↑e j) (Pi.single (↑e i) 1)) ↑e ↑e)
erw [this]