mulVec_vecMul — Mathlib

English

Let A ∈ M_{m×n}(α), B ∈ M_{o×n}(α), x ∈ α^n with n finite. Then A *ᵥ (vecMul x B) = (A Bᵀ) *ᵥ x, expressing a compatibility of vecMul with matrix products and the transpose.

Русский

Пусть A ∈ M_{m×n}(α), B ∈ M_{o×n}(α) и x ∈ α^n. Тогда A *ᵥ (vecMul x B) = (A Bᵀ) *ᵥ x, выражая совместимость vecMul с произведениями матриц и транспонированием.

LaTeX

$$$A *ᵥ (\\text{vecMul } x B) = (A B^\\top) *ᵥ x$$$

Lean4

theorem mulVec_vecMul [Fintype n] [Fintype o] (A : Matrix m n α) (B : Matrix o n α) (x : o → α) :
    A *ᵥ (x ᵥ* B) = (A * Bᵀ) *ᵥ x := by rw [← mulVec_mulVec, mulVec_transpose]

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