cfc_star_id

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

URI: https://scilib.ai/kg/mathlib#cfc_star_id

English

The spectrum of the algebra map algebraMap R A r is a subset of {r}.

Русский

Спектр algebraMap R A r является подмножеством {r}.

LaTeX

$$spectrum R (algebraMap R A r) \subseteq \{ r \ }$$

Lean4

theorem cfc_star_id : cfc (star · : R → R) a = star a := by rw [cfc_star .., cfc_id' ..]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru