English
The map (m→A) × (m×n→A) ↦ (n→A) given by v ↦ vᵥ* M is bilinear in its two arguments.
Русский
Отображение (m→A) × (m×n→A) → (n→A), заданное v ↦ vᵥ*M, билинейно по обоим аргументам.
LaTeX
$$VecMulBilin : (m → A) × (Matrix m n A) → Bilinear in v and M via (v,M) ↦ vᵥ*M$$
Lean4
/-- `Matrix.vecMul` as a bilinear map.
When `A` is non-commutative, this can be instantiated as `vecMulBilin A Aᵐᵒᵖ` -/
def vecMulBilin [Fintype m] : (m → A) →ₗ[R] Matrix m n A →ₗ[S] (n → A)
where
toFun
x :=
{ toFun M := x ᵥ* M
map_add' _ _ := vecMul_add _ _ _
map_smul' _ _ := vecMul_smul _ _ _ }
map_add' _ _ := LinearMap.ext fun _ => add_vecMul _ _ _
map_smul' _ _ := LinearMap.ext fun _ => smul_vecMul _ _ _
