toRows₁_fromRows

Mathlib.Data.Matrix.ColumnRowPartitioned

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

English

The first block extracted from fromRows equals the original A1.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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