submatrix_mulVec_equiv — Mathlib

English

Let M ∈ M_{m×n}(α), v ∈ α^o, e₁ : l → m, e₂ : o ≃ n. Then M.submatrix e₁ e₂ *ᵥ v = (M *ᵥ (v ∘ e₂.symm)) ∘ e₁, i.e., changing index via equivalence commutes with vecMul.

Русский

Пусть M ∈ M_{m×n}(α), v ∈ α^o, e₁ : l → m, e₂ : o ≃ n. Тогда M.submatrix e₁ e₂ *ᵥ v = (M *ᵥ (v ∘ e₂.symm)) ∘ e₁, то есть замена индексов через эквивалентность совместима с vecMul.

LaTeX

$$M.submatrix e₁ e₂ *ᵥ v = (M *ᵥ (v ∘ e₂.symm)) ∘ e₁$$

Lean4

theorem submatrix_mulVec_equiv [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : o → α)
    (e₁ : l → m) (e₂ : o ≃ n) : M.submatrix e₁ e₂ *ᵥ v = (M *ᵥ (v ∘ e₂.symm)) ∘ e₁ :=
  funext fun _ => Eq.symm (dotProduct_comp_equiv_symm _ _ _)

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