instOne

Mathlib.Analysis.CStarAlgebra.Multiplier

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

English

The multiplier algebra 𝓜(𝕜, A) has a multiplicative identity whose image in the product is the pair (1,1).

Русский

У множителя 𝓜(𝕜, A) есть умножительный единичный элемент, образ которого в произведении равен паре (1,1).

LaTeX

$$$(1 : 𝓜(𝕜, A)).toProd = 1$$$

Lean4

instance instOne : One 𝓜(𝕜, A) :=
  ⟨⟨1, fun _x _y => rfl⟩⟩

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

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

Разделы

Аффилиация

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