Theorems · Definition · operator theory

LinearPMap.adjointDomain

{𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : InnerProductSpace 𝕜 F] → (E →ₗ.[𝕜] F) → Submodule 𝕜 F

The domain of the adjoint operator. This definition is needed to construct the adjoint operator and the preferred version to use is T.adjoint.domain instead of T.adjointDomain.

Defined in

Mathlib.Analysis.InnerProductSpace.LinearPMap

Cited by

6 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceNormedAddCommGroupInnerProductSpace