toRows₂_fromRows

Mathlib.Data.Matrix.ColumnRowPartitioned

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

English

The second block extracted from fromRows equals the original A2.

Русский

Вторая часть, полученная из fromRows, равна исходной A2.

LaTeX

$$$\\text{toRows₂}(\\text{fromRows } A_1 A_2) = A_2$$$

Lean4

@[simp]
theorem toRows₂_fromRows (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) : toRows₂ (fromRows A₁ A₂) = A₂ :=
  rfl

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

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

Разделы

Аффилиация

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