one_apply_ne'

Mathlib.Analysis.CStarAlgebra.CStarMatrix

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

English

By symmetry, off-diagonal entries of the identity matrix are zero.

Русский

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

LaTeX

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

Lean4

theorem one_apply_ne' {i j} : j ≠ i → (1 : CStarMatrix n n A) i j = 0 :=
  Matrix.one_apply_ne'

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

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

Разделы

Аффилиация

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