toCols₂_apply

Mathlib.Data.Matrix.ColumnRowPartitioned

URI: https://scilib.ai/kg/mathlib#Matrix.toCols₂_apply

English

From a column-partitioned matrix A, the second block column satisfies (toCols₂ A) i j = A i (Sum.inr j).

Русский

Из колоночной разбиённой матрицы A второй блочный столбец: (toCols₂ A) i j = A i (Sum.inr j).

LaTeX

$$$(toCols₂ A)_{i j} = A_{i,(Sum.inr j)}$$$

Lean4

@[simp]
theorem toCols₂_apply (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₂) : (toCols₂ A) i j = A i (Sum.inr j) :=
  rfl

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

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

Разделы

Аффилиация

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