case a.h
ι : Type u_1
ι' : Type u_2
κ : Type ?u.604344
κ' : Type ?u.604347
R : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
R₂ : Type ?u.604540
M₂ : Type ?u.604543
inst✝¹⁰ : CommRing R₂
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
N : Type ?u.605288
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Fintype κ
inst✝³ : Fintype κ'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
i✝ x✝ : ι'
⊢ toMatrix (reindex b e) v i✝ x✝ = ↑(reindexAlgEquiv R e) (toMatrix b (v ∘ ↑e)) i✝ x✝
ι : Type u_1
ι' : Type u_2
κ : Type ?u.604344
κ' : Type ?u.604347
R : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
R₂ : Type ?u.604540
M₂ : Type ?u.604543
inst✝¹⁰ : CommRing R₂
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
N : Type ?u.605288
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Fintype κ
inst✝³ : Fintype κ'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ toMatrix (reindex b e) v = ↑(reindexAlgEquiv R e) (toMatrix b (v ∘ ↑e))
ext
no goals
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type ?u.604344
κ' : Type ?u.604347
R : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
R₂ : Type ?u.604540
M₂ : Type ?u.604543
inst✝¹⁰ : CommRing R₂
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
N : Type ?u.605288
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Fintype κ
inst✝³ : Fintype κ'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
i✝ x✝ : ι'
⊢ toMatrix (reindex b e) v i✝ x✝ = ↑(reindexAlgEquiv R e) (toMatrix b (v ∘ ↑e)) i✝ x✝
simp only [Basis.toMatrix_apply, Basis.repr_reindex, Matrix.reindexAlgEquiv_apply,
  Matrix.reindex_apply, Matrix.submatrix_apply, Function.comp_apply, e.apply_symm_apply,
  Finsupp.mapDomain_equiv_apply]