Dual space, linear maps and matrices. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains some results on the matrix corresponding to the transpose of a linear map (in the dual space).
Tags #
matrix, linear_map, transpose, dual
@[simp]
theorem
linear_map.to_matrix_transpose
{K : Type u_1}
{V₁ : Type u_2}
{V₂ : Type u_3}
{ι₁ : Type u_4}
{ι₂ : Type u_5}
[field K]
[add_comm_group V₁]
[module K V₁]
[add_comm_group V₂]
[module K V₂]
[fintype ι₁]
[fintype ι₂]
[decidable_eq ι₁]
[decidable_eq ι₂]
{B₁ : basis ι₁ K V₁}
{B₂ : basis ι₂ K V₂}
(u : V₁ →ₗ[K] V₂) :
⇑(linear_map.to_matrix B₂.dual_basis B₁.dual_basis) (⇑module.dual.transpose u) = (⇑(linear_map.to_matrix B₁ B₂) u).transpose
@[simp]
theorem
matrix.to_lin_transpose
{K : Type u_1}
{V₁ : Type u_2}
{V₂ : Type u_3}
{ι₁ : Type u_4}
{ι₂ : Type u_5}
[field K]
[add_comm_group V₁]
[module K V₁]
[add_comm_group V₂]
[module K V₂]
[fintype ι₁]
[fintype ι₂]
[decidable_eq ι₁]
[decidable_eq ι₂]
{B₁ : basis ι₁ K V₁}
{B₂ : basis ι₂ K V₂}
(M : matrix ι₁ ι₂ K) :
⇑(matrix.to_lin B₁.dual_basis B₂.dual_basis) M.transpose = ⇑module.dual.transpose (⇑(matrix.to_lin B₂ B₁) M)