intCast_fst

Mathlib.Analysis.CStarAlgebra.Multiplier

URI: https://scilib.ai/kg/mathlib#DoubleCentralizer.intCast_fst

English

For every integer n, the fst component of n in the multiplier algebra acts as multiplication by n on A.

Русский

Для каждого целого числа n fst-компонента n в умножителе действует умножение на n на A.

LaTeX

$$$ (n : \\mathcal{M}(\\mathbb{K}, A)).\\mathrm{fst} = n \\cdot \\mathrm{id}_A $$$

Lean4

theorem intCast_fst (n : ℤ) : (n : 𝓜(𝕜, A)).fst = n :=
  rfl

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

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

Разделы

Аффилиация

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