R : Type u_2
R₁ : Type ?u.1708981
R₂ : Type ?u.1708984
M : Type ?u.1708987
M₁ : Type u_3
M₂ : Type u_5
M₁' : Type ?u.1708996
M₂' : Type ?u.1708999
n : Type u_7
m : Type u_6
n' : Type u_1
m' : Type u_4
ι : Type ?u.1709014
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'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ (↑(toMatrix c₁ b₁) id)ᵀ ⬝ ↑(toMatrix₂ b₁ b₂) B ⬝ ↑(toMatrix c₂ b₂) id = ↑(toMatrix₂ c₁ c₂) B
R : Type u_2
R₁ : Type ?u.1708981
R₂ : Type ?u.1708984
M : Type ?u.1708987
M₁ : Type u_3
M₂ : Type u_5
M₁' : Type ?u.1708996
M₂' : Type ?u.1708999
n : Type u_7
m : Type u_6
n' : Type u_1
m' : Type u_4
ι : Type ?u.1709014
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'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ (Basis.toMatrix b₁ ↑c₁)ᵀ ⬝ ↑(toMatrix₂ b₁ b₂) B ⬝ Basis.toMatrix b₂ ↑c₂ = ↑(toMatrix₂ c₁ c₂) B
simp_rw [← LinearMap.toMatrix_id_eq_basis_toMatrix]
no goals
R : Type u_2
R₁ : Type ?u.1708981
R₂ : Type ?u.1708984
M : Type ?u.1708987
M₁ : Type u_3
M₂ : Type u_5
M₁' : Type ?u.1708996
M₂' : Type ?u.1708999
n : Type u_7
m : Type u_6
n' : Type u_1
m' : Type u_4
ι : Type ?u.1709014
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'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ (↑(toMatrix c₁ b₁) id)ᵀ ⬝ ↑(toMatrix₂ b₁ b₂) B ⬝ ↑(toMatrix c₂ b₂) id = ↑(toMatrix₂ c₁ c₂) B
rw [← LinearMap.toMatrix₂_compl₁₂, LinearMap.compl₁₂_id_id]