`BookProof.StoneEigenflow.isSelfAdjointExtension_eigenvector` {D Dom : Submodule ℂ F} {Hc : D →ₗ[ℂ] F} {A : Dom →ₗ[ℂ] F} (h : IsSelfAdjointExtension Hc A) (x : D) {lam : ℂ} (hx : H

Initializing...

`BookProof.StoneEigenflow.isSelfAdjointExtension_eigenvector` {D Dom : Submodule ℂ F} {Hc : D →ₗ[ℂ] F} {A : Dom →ₗ[ℂ] F} (h : IsSelfAdjointExtension Hc A) (x : D) {lam : ℂ} (hx : H · Prove2Me