toRows₁_apply

Mathlib.Data.Matrix.ColumnRowPartitioned

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

English

For a partitioned matrix A, the 1st row block satisfies (toRows₁ A) i j = A (Sum.inl i) j.

Русский

Для частичной матрицы A блочный первый ряд удовлетворяет (toRows₁ A) i j = A (Sum.inl i) j.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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