R : Type u_1
R₁ : Type ?u.1586479
R₂ : Type ?u.1586482
M : Type ?u.1586485
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type ?u.1586497
n : Type u_7
m : Type u_5
n' : Type u_6
m' : Type ?u.1586509
ι : Type ?u.1586512
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₁' →ₗ[R] M₁
⊢ (↑(toMatrix b₁' b₁) f)ᵀ ⬝ ↑(toMatrix₂ b₁ b₂) B ⬝ ↑(toMatrix b₂ b₂) id = (↑(toMatrix b₁' b₁) f)ᵀ ⬝ ↑(toMatrix₂ b₁ b₂) B
R : Type u_1
R₁ : Type ?u.1586479
R₂ : Type ?u.1586482
M : Type ?u.1586485
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type ?u.1586497
n : Type u_7
m : Type u_5
n' : Type u_6
m' : Type ?u.1586509
ι : Type ?u.1586512
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₁' →ₗ[R] M₁
⊢ ↑(toMatrix₂ b₁' b₂) (comp B f) = (↑(toMatrix b₁' b₁) f)ᵀ ⬝ ↑(toMatrix₂ b₁ b₂) B
rw [← LinearMap.compl₂_id (B.comp f), ← LinearMap.compl₁₂, LinearMap.toMatrix₂_compl₁₂ b₁ b₂]
no goals
R : Type u_1
R₁ : Type ?u.1586479
R₂ : Type ?u.1586482
M : Type ?u.1586485
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type u_4
M₂' : Type ?u.1586497
n : Type u_7
m : Type u_5
n' : Type u_6
m' : Type ?u.1586509
ι : Type ?u.1586512
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₁' →ₗ[R] M₁
⊢ (↑(toMatrix b₁' b₁) f)ᵀ ⬝ ↑(toMatrix₂ b₁ b₂) B ⬝ ↑(toMatrix b₂ b₂) id = (↑(toMatrix b₁' b₁) f)ᵀ ⬝ ↑(toMatrix₂ b₁ b₂) B
simp