row_submatrix — Mathlib

English

If A is a matrix and r, c define a submatrix A.submatrix r c, then the i-th row of the submatrix equals the i-th row of A with row index mapped by r: (A.submatrix r c).row i = (A.submatrix id c).row (r i).

Русский

Пусть A — матрица, а r, c задают подматрицу A.submatrix r c; i-я строка подматрицы равна i-й строке A после применения r к индексу строки: (A.submatrix r c).row i = (A.submatrix id c).row (r i).

LaTeX

$$$(A.submatrix r c).row i = (A.submatrix id c).row (r i)$$$

Lean4

theorem row_submatrix {m₀ n₀ : Type*} (A : Matrix m n α) (r : m₀ → m) (c : n₀ → n) (i : m₀) :
    (A.submatrix r c).row i = (A.submatrix id c).row (r i) :=
  rfl

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