vecMul_mulVec — Mathlib

English

For A ∈ M_{m×n}(α), B ∈ M_{m×o}(α) and x ∈ α^n, we have (A *ᵥ x) ᵥ* B = x ᵥ* (Aᵀ * B), expressing a composite bilinear interaction.

Русский

Для A ∈ M_{m×n}(α), B ∈ M_{m×o}(α) и x ∈ α^n выполняется (A *ᵥ x) ᵥ* B = x ᵥ* (Aᵀ * B), выражая составную билинейную связь.

LaTeX

$$$(A *ᵥ x) ᵥ* B = x ᵥ* (A^\\top B)$$$

Lean4

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

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