ι : Type u_1
ι' : Type u_2
κ : Type u_5
κ' : Type ?u.502195
R : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
R₂ : Type ?u.502388
M₂ : Type ?u.502391
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 ι
inst✝ : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
this : ↑(toMatrix b₁ b₃) (↑(toLin b₁ b₃) A) ⬝ Basis.toMatrix b₁ ↑b₂ = ↑(toMatrix b₂ b₃) (↑(toLin b₁ b₃) A)
⊢ A ⬝ Basis.toMatrix b₁ ↑b₂ = ↑(toMatrix b₂ b₃) (↑(toLin b₁ b₃) A)
ι : Type u_1
ι' : Type u_2
κ : Type u_5
κ' : Type ?u.502195
R : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
R₂ : Type ?u.502388
M₂ : Type ?u.502391
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 ι
inst✝ : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
⊢ A ⬝ Basis.toMatrix b₁ ↑b₂ = ↑(toMatrix b₂ b₃) (↑(toLin b₁ b₃) A)
have := linearMap_toMatrix_mul_basis_toMatrix b₂ b₁ b₃ (Matrix.toLin b₁ b₃ A)
no goals
ι : Type u_1
ι' : Type u_2
κ : Type u_5
κ' : Type ?u.502195
R : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
R₂ : Type ?u.502388
M₂ : Type ?u.502391
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 ι
inst✝ : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
this : ↑(toMatrix b₁ b₃) (↑(toLin b₁ b₃) A) ⬝ Basis.toMatrix b₁ ↑b₂ = ↑(toMatrix b₂ b₃) (↑(toLin b₁ b₃) A)
⊢ A ⬝ Basis.toMatrix b₁ ↑b₂ = ↑(toMatrix b₂ b₃) (↑(toLin b₁ b₃) A)
rwa [LinearMap.toMatrix_toLin] at this