ι : Type u_2
ι' : Type u_5
κ : Type u_1
κ' : Type ?u.448557
R : Type u_3
M : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
R₂ : Type ?u.448750
M₂ : Type ?u.448753
inst✝⁹ : CommRing R₂
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_6
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 κ
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix ι' κ R
this : Basis.toMatrix b₁ ↑b₂ ⬝ ↑(toMatrix b₃ b₂) (↑(toLin b₃ b₂) A) = ↑(toMatrix b₃ b₁) (↑(toLin b₃ b₂) A)
⊢ Basis.toMatrix b₁ ↑b₂ ⬝ A = ↑(toMatrix b₃ b₁) (↑(toLin b₃ b₂) A)
ι : Type u_2
ι' : Type u_5
κ : Type u_1
κ' : Type ?u.448557
R : Type u_3
M : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
R₂ : Type ?u.448750
M₂ : Type ?u.448753
inst✝⁹ : CommRing R₂
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_6
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 κ
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix ι' κ R
⊢ Basis.toMatrix b₁ ↑b₂ ⬝ A = ↑(toMatrix b₃ b₁) (↑(toLin b₃ b₂) A)
have := basis_toMatrix_mul_linearMap_toMatrix b₃ b₁ b₂ (Matrix.toLin b₃ b₂ A)
no goals
ι : Type u_2
ι' : Type u_5
κ : Type u_1
κ' : Type ?u.448557
R : Type u_3
M : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
R₂ : Type ?u.448750
M₂ : Type ?u.448753
inst✝⁹ : CommRing R₂
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_6
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 κ
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix ι' κ R
this : Basis.toMatrix b₁ ↑b₂ ⬝ ↑(toMatrix b₃ b₂) (↑(toLin b₃ b₂) A) = ↑(toMatrix b₃ b₁) (↑(toLin b₃ b₂) A)
⊢ Basis.toMatrix b₁ ↑b₂ ⬝ A = ↑(toMatrix b₃ b₁) (↑(toLin b₃ b₂) A)
rwa [LinearMap.toMatrix_toLin] at this