Theorems · Theorem · functional analysis

Module.End.mem_invtSubmodule_adjoint_iff

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {U : Submodule 𝕜 E},
  U ∈ Module.End.invtSubmodule (LinearMap.adjoint T) ↔ Uᗮ ∈ Module.End.invtSubmodule T

The linear map version of ContinuousLinearMap.mem_invtSubmodule_adjoint_iff in a finite-dimensional space.

Defined in

Mathlib.Analysis.InnerProductSpace.Adjoint

Cited by

0 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceFiniteDimensional