toCols₁_fromCols

Mathlib.Data.Matrix.ColumnRowPartitioned

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

English

Taking fromCols of A1 and A2 and then toCols₁ recovers A1.

Русский

Из fromCols(A1,A2) и затем toCols₁ получается A1.

LaTeX

$$$\\text{toCols₁}(\\text{fromCols}(A_1,A_2)) = A_1$$$

Lean4

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

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

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

Разделы

Аффилиация

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