ι : Type ?u.327501
ι' : Type u_1
κ : Type u_2
κ' : Type u_4
R : Type u_3
M : Type u_6
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
R₂ : Type ?u.327703
M₂ : Type ?u.327706
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_5
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✝ : DecidableEq ι'
this : DecidableEq κ'
⊢ ↑(toLin b' c) (Basis.toMatrix c ↑c' ⬝ ↑(toMatrix b' c') f) = ↑(toLin b' c) (↑(toMatrix b' c) f)
ι : Type ?u.327501
ι' : Type u_1
κ : Type u_2
κ' : Type u_4
R : Type u_3
M : Type u_6
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
R₂ : Type ?u.327703
M₂ : Type ?u.327706
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_5
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✝ : DecidableEq ι'
⊢ ↑(toLin b' c) (Basis.toMatrix c ↑c' ⬝ ↑(toMatrix b' c') f) = ↑(toLin b' c) (↑(toMatrix b' c) f)
haveI := Classical.decEq κ'
no goals
ι : Type ?u.327501
ι' : Type u_1
κ : Type u_2
κ' : Type u_4
R : Type u_3
M : Type u_6
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
R₂ : Type ?u.327703
M₂ : Type ?u.327706
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_5
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✝ : DecidableEq ι'
this : DecidableEq κ'
⊢ ↑(toLin b' c) (Basis.toMatrix c ↑c' ⬝ ↑(toMatrix b' c') f) = ↑(toLin b' c) (↑(toMatrix b' c) f)
rw [toLin_toMatrix, toLin_mul b' c' c, toLin_toMatrix, c.toLin_toMatrix, id_comp]