toCols₂_fromCols

Mathlib.Data.Matrix.ColumnRowPartitioned

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

English

The second block of columns of a column-assembled matrix is exactly A2.

Русский

Второй блок столбцов составной матрицы равен A2.

LaTeX

$$$\operatorname{toCols}_2(\operatorname{fromCols}(A_1,A_2)) = A_2$$$

Lean4

@[simp]
theorem toCols₂_fromCols (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) : toCols₂ (fromCols A₁ A₂) = A₂ :=
  rfl

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

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

Разделы

Аффилиация

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