fromCols_apply_inr

Mathlib.Data.Matrix.ColumnRowPartitioned

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

English

In the fromCols construction, the right block corresponds to A2 on Sum.inr indices.

Русский

В конструкторе fromCols правая часть соответствует A2 на индексах Sum.inr.

LaTeX

$$$(\\text{fromCols}(A_1,A_2)) i (\\text{Sum.inr } j) = A_2 i j$$$

Lean4

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

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

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

Разделы

Аффилиация

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