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]