submatrix_map — Mathlib

English

Applying a function to all entries commutes with submatrix: (A.map f).submatrix e1 e2 = (A.submatrix e1 e2).map f.

Русский

Применение функции ко всем элементам матрицы commute с подматрицей: (A.map f).submatrix e1 e2 = (A.submatrix e1 e2).map f.

LaTeX

$$$ (A.map f).submatrix e_1 e_2 = (A.submatrix e_1 e_2).map f $$$

Lean4

theorem submatrix_map (f : α → β) (e₁ : l → m) (e₂ : o → n) (A : Matrix m n α) :
    (A.map f).submatrix e₁ e₂ = (A.submatrix e₁ e₂).map f :=
  rfl

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