one_apply_ne

Mathlib.Analysis.CStarAlgebra.CStarMatrix

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

English

Off-diagonal entries of the identity matrix are zero.

Русский

Вне диагонали элементы единичной матрицы равны нулю.

LaTeX

$$$\bigl(1: CStarMatrix\, n\, n\, A\bigr)_{ij} = 0 \quad\text{если } i \neq j$$$

Lean4

@[simp]
theorem one_apply_ne {i j} : i ≠ j → (1 : CStarMatrix n n A) i j = 0 :=
  Matrix.one_apply_ne

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

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

Разделы

Аффилиация

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