row_submatrix_eq_comp — Mathlib

English

The i-th row of a submatrix equals the i-th row of A composed with c: (A.submatrix r c).row i = A.row (r i) ∘ c.

Русский

i-я строка подматрицы равна i-й строке A после композиции с c: (A.submatrix r c).row i = A.row (r i) ∘ c.

LaTeX

$$$(A.submatrix r c).row i = A.row (r i) \circ c$$$

Lean4

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

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