one_apply_eq

Mathlib.Analysis.CStarAlgebra.CStarMatrix

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

English

For every i, the i,i entry of the identity matrix is 1.

Русский

Для каждого i диагональный элемент единичной матрицы равен 1.

LaTeX

$$$\bigl(1: CStarMatrix\, n\, n\, A\bigr)_{ii} = 1\quad\text{для всех } i$$$

Lean4

@[simp]
theorem one_apply_eq (i) : (1 : CStarMatrix n n A) i i = 1 :=
  Matrix.one_apply_eq _

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

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

Разделы

Аффилиация

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