cfcₙ_star_id

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

URI: https://scilib.ai/kg/mathlib#cfcₙ_star_id

English

The nonunital calculus respects the involution on scalars: cfc_n (star ·) a = star a.

Русский

Калькулятор сохраняет звезду от скаляров: cfc_n(star ·) a = star a.

LaTeX

$$$$ cfc\\!_n(\\text{star} \\cdot)\\ a = \\text{star}\;a $$$$

Lean4

theorem cfcₙ_star_id : cfcₙ (star · : R → R) a = star a := by rw [cfcₙ_star _ a, cfcₙ_id' R a]

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

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

Разделы

Аффилиация

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