case a
K : Type u_3
V₁ : Type u_4
V₂ : Type u_5
ι₁ : Type u_1
ι₂ : Type u_2
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
⊢ ↑(LinearMap.toMatrix (Basis.dualBasis B₁) (Basis.dualBasis B₂))
      (↑(toLin (Basis.dualBasis B₁) (Basis.dualBasis B₂)) Mᵀ) =
    ↑(LinearMap.toMatrix (Basis.dualBasis B₁) (Basis.dualBasis B₂)) (↑Module.Dual.transpose (↑(toLin B₂ B₁) M))
K : Type u_3
V₁ : Type u_4
V₂ : Type u_5
ι₁ : Type u_1
ι₂ : Type u_2
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
⊢ ↑(toLin (Basis.dualBasis B₁) (Basis.dualBasis B₂)) Mᵀ = ↑Module.Dual.transpose (↑(toLin B₂ B₁) M)
apply (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis).injective
no goals
case a
K : Type u_3
V₁ : Type u_4
V₂ : Type u_5
ι₁ : Type u_1
ι₂ : Type u_2
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
⊢ ↑(LinearMap.toMatrix (Basis.dualBasis B₁) (Basis.dualBasis B₂))
      (↑(toLin (Basis.dualBasis B₁) (Basis.dualBasis B₂)) Mᵀ) =
    ↑(LinearMap.toMatrix (Basis.dualBasis B₁) (Basis.dualBasis B₂)) (↑Module.Dual.transpose (↑(toLin B₂ B₁) M))
rw [LinearMap.toMatrix_toLin, LinearMap.toMatrix_transpose, LinearMap.toMatrix_toLin]