algebraMap_snd

Mathlib.Analysis.CStarAlgebra.Multiplier

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

English

The ring structure on 𝓜(𝕜,A) is obtained by pulling back the product structure along the injective map toProdMulOpposite.

Русский

Кольцевая структура на 𝓜(𝕜,A) задаётся переносом произведения через инъекцию toProdMulOpposite.

LaTeX

$$$\\text{pullback ring structure}$$$

Lean4

theorem algebraMap_snd (k : 𝕜) : (algebraMap 𝕜 𝓜(𝕜, A) k).snd = algebraMap 𝕜 _ k :=
  rfl

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

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

Разделы

Аффилиация

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