col_submatrix — Mathlib

English

The j-th column of the submatrix equals the j-th column of A restricted by r: (A.submatrix r c).col j = (A.submatrix r id).col (c j).

Русский

j-й столбец подматрицы равен j-му столбцу A, ограниченному по r: (A.submatrix r c).col j = (A.submatrix r id).col (c j).

LaTeX

$$$(A.submatrix r c).col j = (A.submatrix r id).col (c j)$$$

Lean4

theorem col_submatrix {m₀ n₀ : Type*} (A : Matrix m n α) (r : m₀ → m) (c : n₀ → n) (j : n₀) :
    (A.submatrix r c).col j = (A.submatrix r id).col (c j) :=
  rfl

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