star_apply

Mathlib.Analysis.CStarAlgebra.CStarMatrix

URI: https://scilib.ai/kg/mathlib#CStarMatrix.star_apply

English

The star operation on matrices satisfies (star f)_{i j} = star(f_{j i}).

Русский

Операция звезды на матрицах удовлетворяет (star f)_{i j} = star(f_{j i}).

LaTeX

$$$[Star A] {f : CStarMatrix n n A} {i j : n} : (star f)_{i j} = star (f_{j i})$$$

Lean4

theorem star_apply [Star A] {f : CStarMatrix n n A} {i j : n} : (star f) i j = star (f j i) := by
  rw [star_eq_conjTranspose, conjTranspose_apply]

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

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

Разделы

Аффилиация

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