single_apply_of_col_ne

Mathlib.Data.Matrix.Basis

URI: https://scilib.ai/kg/mathlib#Matrix.single_apply_of_col_ne

English

If j ≠ j', then the entry (i, j') of single i j a is zero for all i.

Русский

Если j ≠ j', то элемент (i, j') единичной матрицы на позиции (i, j) равняется нулю для любого i.

LaTeX

$$$ \mathrm{single}_{i j} a \_{i j'} = 0 \quad \text{if } j \neq j' $$$

Lean4

theorem single_apply_of_col_ne (i i' : m) {j j' : n} (hj : j ≠ j') (a : α) : single i j a i' j' = 0 := by simp [hj]

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

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

Разделы

Аффилиация

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