theorem AdjointOperators.adjoint_inner_right_property {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (v w : E) : inner 𝕜 (T v) w = inner 𝕜 v ((LinearMap.adjoint T) w)

def AdjointOperators.IsNormalOperator {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) : Prop

theorem AdjointOperators.adjoint_maps_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (W : Submodule 𝕜 E) (hW : ∀ w ∈ W, T w ∈ W) (u : E) : u ∈ Wᗮ → (LinearMap.adjoint T) u ∈ Wᗮ

theorem AdjointOperators.norm_apply_eq_norm_adjoint_of_normal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (hN : T ∘ₗ LinearMap.adjoint T = LinearMap.adjoint T ∘ₗ T) (v : E) : ‖T v‖ = ‖(LinearMap.adjoint T) v‖

theorem AdjointOperators.normal_adjoint_eigenvalue {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (hN : T ∘ₗ LinearMap.adjoint T = LinearMap.adjoint T ∘ₗ T) (v : E) (μ : 𝕜) (hv : T v = μ • v) : (LinearMap.adjoint T) v = (starRingEnd 𝕜) μ • v