ι : Type u_1
ι' : Type u_2
κ : Type ?u.583643
κ' : Type ?u.583646
R : Type u_3
M : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
R₂ : Type ?u.583839
M₂ : Type ?u.583842
inst✝⁹ : CommRing R₂
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type ?u.584587
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 ι
this : DecidableEq ι'
⊢ ↑(toMatrix b b') id = Basis.toMatrix b' ↑b
ι : Type u_1
ι' : Type u_2
κ : Type ?u.583643
κ' : Type ?u.583646
R : Type u_3
M : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
R₂ : Type ?u.583839
M₂ : Type ?u.583842
inst✝⁹ : CommRing R₂
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type ?u.584587
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 ι
⊢ ↑(toMatrix b b') id = Basis.toMatrix b' ↑b
haveI := Classical.decEq ι'
no goals
ι : Type u_1
ι' : Type u_2
κ : Type ?u.583643
κ' : Type ?u.583646
R : Type u_3
M : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
R₂ : Type ?u.583839
M₂ : Type ?u.583842
inst✝⁹ : CommRing R₂
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type ?u.584587
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 ι
this : DecidableEq ι'
⊢ ↑(toMatrix b b') id = Basis.toMatrix b' ↑b
rw [← @basis_toMatrix_mul_linearMap_toMatrix _ _ ι, toMatrix_id, Matrix.mul_one]