toEuclideanLin_conjTranspose_eq_adjoint

English

The linear map associated to the conjugate transpose of a matrix A is the adjoint of the linear map associated to A; i.e., toLin(conjTranspose A) = adjoint(toLin A).

Русский

Линейное отображение, соответствующее коньюгатно-транспонированной матрице A, равно сопряжённому отображению к линейному отображению, соответствующему A; то есть toLin(Aᴴ) = adjoint(toLin A).

LaTeX

$$$\operatorname{toLin}(A^{\mathsf{H}}) = \operatorname{adjoint}(\operatorname{toLin}(A))$$$

Lean4

/-- The adjoint of the linear map associated to a matrix is the linear map associated to the
conjugate transpose of that matrix. -/
theorem toEuclideanLin_conjTranspose_eq_adjoint (A : Matrix m n 𝕜) :
    A.conjTranspose.toEuclideanLin = A.toEuclideanLin.adjoint :=
  A.toLin_conjTranspose (EuclideanSpace.basisFun n 𝕜) (EuclideanSpace.basisFun m 𝕜)

Похожие утверждения