case h
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 α
b✝ : n → α
A : Matrix m m α
e : n ≃ m
b : n → α
i : n
⊢ ↑(cramer (submatrix A ↑e ↑e)) b i = (↑(cramer A) (b ∘ ↑e.symm) ∘ ↑e) 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 α
b✝ : n → α
A : Matrix m m α
e : n ≃ m
b : n → α
⊢ ↑(cramer (submatrix A ↑e ↑e)) b = ↑(cramer A) (b ∘ ↑e.symm) ∘ ↑e
ext i
no goals
case h
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 α
b✝ : n → α
A : Matrix m m α
e : n ≃ m
b : n → α
i : n
⊢ ↑(cramer (submatrix A ↑e ↑e)) b i = (↑(cramer A) (b ∘ ↑e.symm) ∘ ↑e) i
simp_rw [Function.comp_apply, cramer_apply, updateColumn_submatrix_equiv,
  det_submatrix_equiv_self e, Function.comp]