mathlib3 documentation

linear_algebra.matrix.dual

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₂) :
@[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) :