instNonUnitalIsometricContinuousFunctionalCalculus

English

The nonunital isometric continuous functional calculus instance is compatible with IsSelfAdjoint.

Русский

Экземпляр неединичного изометрического непрерывного функционального калькулятора совместим с IsSelfAdjoint.

LaTeX

$$IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus$$

Lean4

instance instNonUnitalIsometricContinuousFunctionalCalculus :
    NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint :=
  QuasispectrumRestricts.isometric_cfc Complex.reCLM Complex.isometry_ofReal (.zero _) fun _ ↦
    isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts

Похожие утверждения