toCols₁_apply

Mathlib.Data.Matrix.ColumnRowPartitioned

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

English

From a column-partitioned matrix A, the first block column satisfies (toCols₁ A) i j = A i (Sum.inl j).

Русский

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

LaTeX

$$$(toCols₁ A)_{i j} = A_{i,(Sum.inl j)}$$$

Lean4

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

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

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

Разделы

Аффилиация

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