# Adjoint of operators on Hilbert spaces #

Given an operator A : E →L[𝕜] F, where E and F are Hilbert spaces, its adjoint adjoint A : F →L[𝕜] E is the unique operator such that ⟪x, A y⟫ = ⟪adjoint A x, y⟫ for all x and y.

We then use this to put a C⋆-algebra structure on E →L[𝕜] E with the adjoint as the star operation.

This construction is used to define an adjoint for linear maps (i.e. not continuous) between finite dimensional spaces.

## Main definitions #

• ContinuousLinearMap.adjoint : (E →L[𝕜] F) ≃ₗᵢ⋆[𝕜] (F →L[𝕜] E): the adjoint of a continuous linear map, bundled as a conjugate-linear isometric equivalence.
• LinearMap.adjoint : (E →ₗ[𝕜] F) ≃ₗ⋆[𝕜] (F →ₗ[𝕜] E): the adjoint of a linear map between finite-dimensional spaces, this time only as a conjugate-linear equivalence, since there is no norm defined on these maps.

## Implementation notes #

• The continuous conjugate-linear version adjointAux is only an intermediate definition and is not meant to be used outside this file.

## Tags #

noncomputable def ContinuousLinearMap.adjointAux {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] :
(E →L[𝕜] F) →L⋆[𝕜] F →L[𝕜] E

The adjoint, as a continuous conjugate-linear map. This is only meant as an auxiliary definition for the main definition adjoint, where this is bundled as a conjugate-linear isometric equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ContinuousLinearMap.adjointAux_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] (A : E →L[𝕜] F) (x : F) :
(ContinuousLinearMap.adjointAux A) x = ().symm ((ContinuousLinearMap.toSesqForm A) x)
theorem ContinuousLinearMap.adjointAux_inner_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] (A : E →L[𝕜] F) (x : E) (y : F) :
(ContinuousLinearMap.adjointAux A) y, x⟫_𝕜 = y, A x⟫_𝕜
theorem ContinuousLinearMap.adjointAux_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] (A : E →L[𝕜] F) (x : E) (y : F) :
x, (ContinuousLinearMap.adjointAux A) y⟫_𝕜 = A x, y⟫_𝕜
theorem ContinuousLinearMap.adjointAux_adjointAux {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) :
@[simp]
theorem ContinuousLinearMap.adjointAux_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) :
def ContinuousLinearMap.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] :
(E →L[𝕜] F) ≃ₗᵢ⋆[𝕜] F →L[𝕜] E

The adjoint of a bounded operator from Hilbert space E to Hilbert space F.

Equations
Instances For
Equations
Instances For
theorem ContinuousLinearMap.adjoint_inner_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) (x : E) (y : F) :
(ContinuousLinearMap.adjoint A) y, x⟫_𝕜 = y, A x⟫_𝕜

The fundamental property of the adjoint.

theorem ContinuousLinearMap.adjoint_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) (x : E) (y : F) :
x, (ContinuousLinearMap.adjoint A) y⟫_𝕜 = A x, y⟫_𝕜

The fundamental property of the adjoint.

@[simp]
theorem ContinuousLinearMap.adjoint_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) :

@[simp]
theorem ContinuousLinearMap.adjoint_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [] [] [] [] [] [] [] (A : F →L[𝕜] G) (B : E →L[𝕜] F) :

The adjoint of the composition of two operators is the composition of the two adjoints in reverse order.

theorem ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) (x : E) :
A x ^ 2 = RCLike.re ((ContinuousLinearMap.adjoint A).comp A) x, x⟫_𝕜
theorem ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) (x : E) :
A x = (RCLike.re ((ContinuousLinearMap.adjoint A).comp A) x, x⟫_𝕜)
theorem ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) (x : E) :
A x ^ 2 = RCLike.re x, ((ContinuousLinearMap.adjoint A).comp A) x⟫_𝕜
theorem ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) (x : E) :
A x = (RCLike.re x, ((ContinuousLinearMap.adjoint A).comp A) x⟫_𝕜)
theorem ContinuousLinearMap.eq_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) (B : F →L[𝕜] E) :
A = ContinuousLinearMap.adjoint B ∀ (x : E) (y : F), A x, y⟫_𝕜 = x, B y⟫_𝕜

The adjoint is unique: a map A is the adjoint of B iff it satisfies ⟪A x, y⟫ = ⟪x, B y⟫ for all x and y.

@[simp]
theorem ContinuousLinearMap.adjoint_id {𝕜 : Type u_1} {E : Type u_2} [] [] [] :
theorem Submodule.adjoint_subtypeL {𝕜 : Type u_1} {E : Type u_2} [] [] [] (U : ) [] :
theorem Submodule.adjoint_orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [] [] [] (U : ) [] :
instance ContinuousLinearMap.instStarId {𝕜 : Type u_1} {E : Type u_2} [] [] [] :
Star (E →L[𝕜] E)

E →L[𝕜] E is a star algebra with the adjoint as the star operation.

Equations
• ContinuousLinearMap.instStarId = { star := ContinuousLinearMap.adjoint }
instance ContinuousLinearMap.instInvolutiveStarId {𝕜 : Type u_1} {E : Type u_2} [] [] [] :
Equations
• ContinuousLinearMap.instInvolutiveStarId =
instance ContinuousLinearMap.instStarMulId {𝕜 : Type u_1} {E : Type u_2} [] [] [] :
StarMul (E →L[𝕜] E)
Equations
• ContinuousLinearMap.instStarMulId =
instance ContinuousLinearMap.instStarRingId {𝕜 : Type u_1} {E : Type u_2} [] [] [] :
StarRing (E →L[𝕜] E)
Equations
• ContinuousLinearMap.instStarRingId =
instance ContinuousLinearMap.instStarModuleId {𝕜 : Type u_1} {E : Type u_2} [] [] [] :
StarModule 𝕜 (E →L[𝕜] E)
Equations
• =
theorem ContinuousLinearMap.star_eq_adjoint {𝕜 : Type u_1} {E : Type u_2} [] [] [] (A : E →L[𝕜] E) :
theorem ContinuousLinearMap.isSelfAdjoint_iff' {𝕜 : Type u_1} {E : Type u_2} [] [] [] {A : E →L[𝕜] E} :

A continuous linear operator is self-adjoint iff it is equal to its adjoint.

theorem ContinuousLinearMap.norm_adjoint_comp_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) :
(ContinuousLinearMap.adjoint A).comp A = A * A
instance ContinuousLinearMap.instCstarRingId {𝕜 : Type u_1} {E : Type u_2} [] [] [] :
CstarRing (E →L[𝕜] E)
Equations
• =
theorem ContinuousLinearMap.isAdjointPair_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →L[𝕜] F) :

theorem IsSelfAdjoint.adjoint_eq {𝕜 : Type u_1} {E : Type u_2} [] [] [] {A : E →L[𝕜] E} (hA : ) :
theorem IsSelfAdjoint.isSymmetric {𝕜 : Type u_1} {E : Type u_2} [] [] [] {A : E →L[𝕜] E} (hA : ) :
(A).IsSymmetric

Every self-adjoint operator on an inner product space is symmetric.

theorem IsSelfAdjoint.conj_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] {T : E →L[𝕜] E} (hT : ) (S : E →L[𝕜] F) :

theorem IsSelfAdjoint.adjoint_conj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] {T : E →L[𝕜] E} (hT : ) (S : F →L[𝕜] E) :

theorem ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric {𝕜 : Type u_1} {E : Type u_2} [] [] [] {A : E →L[𝕜] E} :
(A).IsSymmetric
theorem LinearMap.IsSymmetric.isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [] [] [] {A : E →L[𝕜] E} (hA : (A).IsSymmetric) :
theorem orthogonalProjection_isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [] [] [] (U : ) [] :

theorem IsSelfAdjoint.conj_orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [] [] [] {T : E →L[𝕜] E} (hT : ) (U : ) [] :
IsSelfAdjoint (U.subtypeL.comp (.comp (T.comp (U.subtypeL.comp ))))
def LinearMap.IsSymmetric.toSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [] [] [] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :

The Hellinger--Toeplitz theorem: Construct a self-adjoint operator from an everywhere defined symmetric operator.

Equations
• hT.toSelfAdjoint = { toLinearMap := T, cont := },
Instances For
theorem LinearMap.IsSymmetric.coe_toSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [] [] [] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :
theorem LinearMap.IsSymmetric.toSelfAdjoint_apply {𝕜 : Type u_1} {E : Type u_2} [] [] [] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {x : E} :
def LinearMap.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] :
(E →ₗ[𝕜] F) ≃ₗ⋆[𝕜] F →ₗ[𝕜] E

The adjoint of an operator from the finite-dimensional inner product space E to the finite-dimensional inner product space F.

Equations
• LinearMap.adjoint = let_fun this := ; let_fun this_1 := ; (LinearMap.toContinuousLinearMap.trans ContinuousLinearMap.adjoint.toLinearEquiv).trans LinearMap.toContinuousLinearMap.symm
Instances For
theorem LinearMap.adjoint_toContinuousLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →ₗ[𝕜] F) :
theorem LinearMap.adjoint_eq_toCLM_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →ₗ[𝕜] F) :
theorem LinearMap.adjoint_inner_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →ₗ[𝕜] F) (x : E) (y : F) :
(LinearMap.adjoint A) y, x⟫_𝕜 = y, A x⟫_𝕜

The fundamental property of the adjoint.

theorem LinearMap.adjoint_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →ₗ[𝕜] F) (x : E) (y : F) :
x, (LinearMap.adjoint A) y⟫_𝕜 = A x, y⟫_𝕜

The fundamental property of the adjoint.

@[simp]
theorem LinearMap.adjoint_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →ₗ[𝕜] F) :

@[simp]
theorem LinearMap.adjoint_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [] [] [] [] [] [] [] (A : F →ₗ[𝕜] G) (B : E →ₗ[𝕜] F) :

The adjoint of the composition of two operators is the composition of the two adjoints in reverse order.

theorem LinearMap.eq_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
A = LinearMap.adjoint B ∀ (x : E) (y : F), A x, y⟫_𝕜 = x, B y⟫_𝕜

The adjoint is unique: a map A is the adjoint of B iff it satisfies ⟪A x, y⟫ = ⟪x, B y⟫ for all x and y.

theorem LinearMap.eq_adjoint_iff_basis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] {ι₁ : Type u_5} {ι₂ : Type u_6} (b₁ : Basis ι₁ 𝕜 E) (b₂ : Basis ι₂ 𝕜 F) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
A = LinearMap.adjoint B ∀ (i₁ : ι₁) (i₂ : ι₂), A (b₁ i₁), b₂ i₂⟫_𝕜 = b₁ i₁, B (b₂ i₂)⟫_𝕜

The adjoint is unique: a map A is the adjoint of B iff it satisfies ⟪A x, y⟫ = ⟪x, B y⟫ for all basis vectors x and y.

theorem LinearMap.eq_adjoint_iff_basis_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] {ι : Type u_5} (b : Basis ι 𝕜 E) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
A = LinearMap.adjoint B ∀ (i : ι) (y : F), A (b i), y⟫_𝕜 = b i, B y⟫_𝕜
theorem LinearMap.eq_adjoint_iff_basis_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] {ι : Type u_5} (b : Basis ι 𝕜 F) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
A = LinearMap.adjoint B ∀ (i : ι) (x : E), A x, b i⟫_𝕜 = x, B (b i)⟫_𝕜
instance LinearMap.instStarId {𝕜 : Type u_1} {E : Type u_2} [] [] [] :
Star (E →ₗ[𝕜] E)

E →ₗ[𝕜] E is a star algebra with the adjoint as the star operation.

Equations
• LinearMap.instStarId = { star := LinearMap.adjoint }
instance LinearMap.instInvolutiveStarId {𝕜 : Type u_1} {E : Type u_2} [] [] [] :
Equations
• LinearMap.instInvolutiveStarId =
instance LinearMap.instStarMulId {𝕜 : Type u_1} {E : Type u_2} [] [] [] :
StarMul (E →ₗ[𝕜] E)
Equations
• LinearMap.instStarMulId =
instance LinearMap.instStarRingId {𝕜 : Type u_1} {E : Type u_2} [] [] [] :
StarRing (E →ₗ[𝕜] E)
Equations
• LinearMap.instStarRingId =
instance LinearMap.instStarModuleId {𝕜 : Type u_1} {E : Type u_2} [] [] [] :
StarModule 𝕜 (E →ₗ[𝕜] E)
Equations
• =
theorem LinearMap.star_eq_adjoint {𝕜 : Type u_1} {E : Type u_2} [] [] [] (A : E →ₗ[𝕜] E) :
theorem LinearMap.isSelfAdjoint_iff' {𝕜 : Type u_1} {E : Type u_2} [] [] [] {A : E →ₗ[𝕜] E} :

A continuous linear operator is self-adjoint iff it is equal to its adjoint.

theorem LinearMap.isSymmetric_iff_isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [] [] [] (A : E →ₗ[𝕜] E) :
A.IsSymmetric
theorem LinearMap.isAdjointPair_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] (A : E →ₗ[𝕜] F) :
theorem LinearMap.isSymmetric_adjoint_mul_self {𝕜 : Type u_1} {E : Type u_2} [] [] [] (T : E →ₗ[𝕜] E) :

The Gram operator T†T is symmetric.

theorem LinearMap.re_inner_adjoint_mul_self_nonneg {𝕜 : Type u_1} {E : Type u_2} [] [] [] (T : E →ₗ[𝕜] E) (x : E) :
0 RCLike.re x, (LinearMap.adjoint T * T) x⟫_𝕜

The Gram operator T†T is a positive operator.

@[simp]
theorem LinearMap.im_inner_adjoint_mul_self_eq_zero {𝕜 : Type u_1} {E : Type u_2} [] [] [] (T : E →ₗ[𝕜] E) (x : E) :
RCLike.im x, (LinearMap.adjoint T) (T x)⟫_𝕜 = 0
theorem ContinuousLinearMap.inner_map_map_iff_adjoint_comp_self {𝕜 : Type u_1} [] {H : Type u_5} [] [] {K : Type u_6} [] [] (u : H →L[𝕜] K) :
(∀ (x y : H), u x, u y⟫_𝕜 = x, y⟫_𝕜) (ContinuousLinearMap.adjoint u).comp u = 1
theorem ContinuousLinearMap.norm_map_iff_adjoint_comp_self {𝕜 : Type u_1} [] {H : Type u_5} [] [] {K : Type u_6} [] [] (u : H →L[𝕜] K) :
(∀ (x : H), u x = x) (ContinuousLinearMap.adjoint u).comp u = 1
@[simp]
theorem LinearIsometryEquiv.adjoint_eq_symm {𝕜 : Type u_1} [] {H : Type u_5} [] [] {K : Type u_6} [] [] (e : H ≃ₗᵢ[𝕜] K) :
ContinuousLinearMap.adjoint { toLinearEquiv := e.toLinearEquiv, continuous_toFun := , continuous_invFun := } = { toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := , continuous_invFun := }
@[simp]
theorem LinearIsometryEquiv.star_eq_symm {𝕜 : Type u_1} [] {H : Type u_5} [] [] (e : H ≃ₗᵢ[𝕜] H) :
star { toLinearEquiv := e.toLinearEquiv, continuous_toFun := , continuous_invFun := } = { toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := , continuous_invFun := }
theorem ContinuousLinearMap.norm_map_of_mem_unitary {𝕜 : Type u_1} [] {H : Type u_5} [] [] {u : H →L[𝕜] H} (hu : u unitary (H →L[𝕜] H)) (x : H) :
theorem ContinuousLinearMap.inner_map_map_of_mem_unitary {𝕜 : Type u_1} [] {H : Type u_5} [] [] {u : H →L[𝕜] H} (hu : u unitary (H →L[𝕜] H)) (x : H) (y : H) :
u x, u y⟫_𝕜 = x, y⟫_𝕜
theorem unitary.norm_map {𝕜 : Type u_1} [] {H : Type u_5} [] [] (u : (unitary (H →L[𝕜] H))) (x : H) :
u x = x
theorem unitary.inner_map_map {𝕜 : Type u_1} [] {H : Type u_5} [] [] (u : (unitary (H →L[𝕜] H))) (x : H) (y : H) :
u x, u y⟫_𝕜 = x, y⟫_𝕜
noncomputable def unitary.linearIsometryEquiv {𝕜 : Type u_1} [] {H : Type u_5} [] [] :
(unitary (H →L[𝕜] H)) ≃* (H ≃ₗᵢ[𝕜] H)

The unitary elements of continuous linear maps on a Hilbert space coincide with the linear isometric equivalences on that Hilbert space.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem unitary.linearIsometryEquiv_coe_apply {𝕜 : Type u_1} [] {H : Type u_5} [] [] (u : (unitary (H →L[𝕜] H))) :
{ toLinearEquiv := (unitary.linearIsometryEquiv u).toLinearEquiv, continuous_toFun := , continuous_invFun := } = u
@[simp]
theorem unitary.linearIsometryEquiv_coe_symm_apply {𝕜 : Type u_1} [] {H : Type u_5} [] [] (e : H ≃ₗᵢ[𝕜] H) :
(unitary.linearIsometryEquiv.symm e) = { toLinearEquiv := e.toLinearEquiv, continuous_toFun := , continuous_invFun := }
theorem Matrix.toLin_conjTranspose {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] {m : Type u_5} {n : Type u_6} [] [] [] [] [] [] (v₁ : ) (v₂ : ) (A : Matrix m n 𝕜) :
(Matrix.toLin v₂.toBasis v₁.toBasis) A.conjTranspose = LinearMap.adjoint ((Matrix.toLin v₁.toBasis v₂.toBasis) A)

The linear map associated to the conjugate transpose of a matrix corresponding to two orthonormal bases is the adjoint of the linear map associated to the matrix.

theorem LinearMap.toMatrix_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] {m : Type u_5} {n : Type u_6} [] [] [] [] [] [] (v₁ : ) (v₂ : ) (f : E →ₗ[𝕜] F) :
(LinearMap.toMatrix v₂.toBasis v₁.toBasis) (LinearMap.adjoint f) = ((LinearMap.toMatrix v₁.toBasis v₂.toBasis) f).conjTranspose

The matrix associated to the adjoint of a linear map corresponding to two orthonormal bases is the conjugate tranpose of the matrix associated to the linear map.

@[simp]
theorem LinearMap.toMatrixOrthonormal_symm_apply {𝕜 : Type u_1} {E : Type u_2} [] [] {n : Type u_6} [] [] [] (v₁ : ) :
∀ (a : Matrix n n 𝕜), .symm a = (LinearMap.toMatrix v₁.toBasis v₁.toBasis).invFun a
@[simp]
theorem LinearMap.toMatrixOrthonormal_apply {𝕜 : Type u_1} {E : Type u_2} [] [] {n : Type u_6} [] [] [] (v₁ : ) :
∀ (a : E →ₗ[𝕜] E), = ((LinearMap.toMatrix v₁.toBasis v₁.toBasis)).toFun a
def LinearMap.toMatrixOrthonormal {𝕜 : Type u_1} {E : Type u_2} [] [] {n : Type u_6} [] [] [] (v₁ : ) :
(E →ₗ[𝕜] E) ≃⋆ₐ[𝕜] Matrix n n 𝕜

The star algebra equivalence between the linear endomorphisms of finite-dimensional inner product space and square matrices induced by the choice of an orthonormal basis.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Matrix.toEuclideanLin_conjTranspose_eq_adjoint {𝕜 : Type u_1} [] {m : Type u_5} {n : Type u_6} [] [] [] [] (A : Matrix m n 𝕜) :
Matrix.toEuclideanLin A.conjTranspose = LinearMap.adjoint (Matrix.toEuclideanLin A)

The adjoint of the linear map associated to a matrix is the linear map associated to the conjugate transpose of that matrix.