Theorems · Theorem · functional analysis

LinearMap.eq_adjoint_iff_basis

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] {ι₁ : Type u_5} {ι₂ : Type u_6}
  (b₁ : Module.Basis ι₁ 𝕜 E) (b₂ : Module.Basis ι₂ 𝕜 F) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E),
  A = LinearMap.adjoint B ↔ ∀ (i₁ : ι₁) (i₂ : ι₂), inner 𝕜 (A (b₁ i₁)) (b₂ i₂) = inner 𝕜 (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.

Defined in

Mathlib.Analysis.InnerProductSpace.Adjoint

Cited by

1 results in Mathlib

Foundations

Depth 195 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupNormedAddCommGroupInnerProductSpaceInnerProductSpaceFiniteDimensionalFiniteDimensional