map_id'

Mathlib.Analysis.CStarAlgebra.CStarMatrix

URI: https://scilib.ai/kg/mathlib#CStarMatrix.map_id'

English

Applying the identity function entrywise leaves a matrix unchanged: M.map(id) = M.

Русский

Пусть применяется единичная функция по элементам; матрица не меняется: M.map(id) = M.

LaTeX

$$$\\forall M : CStarMatrix m n A, M.map (\\cdot) = M$$$

Lean4

@[simp]
theorem map_id' (M : CStarMatrix m n A) : M.map (·) = M :=
  map_id M

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

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

Разделы

Аффилиация

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