ofMatrix_apply

Mathlib.Analysis.CStarAlgebra.CStarMatrix

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

English

For any matrix M, (ofMatrix M) i = M i for every index i.

Русский

Для любой матрицы M верно (ofMatrix M) i = M i для каждого индекса i.

LaTeX

$$$ (\mathrm{ofMatrix}\ M)\;i = M\;i $$$

Lean4

@[simp]
theorem ofMatrix_apply {M : Matrix m n A} {i : m} : (ofMatrix M) i = M i :=
  rfl

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

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

Разделы

Аффилиация

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