toRows₂_apply

Mathlib.Data.Matrix.ColumnRowPartitioned

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

English

For a partitioned matrix A, the 2nd row block satisfies (toRows₂ A) i j = A (Sum.inr i) j.

Русский

Для частичной матрицы A второй блок строк: (toRows₂ A) i j = A (Sum.inr i) j.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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