English
The operation vecMulVec is a bilinear map from (m→A) × (n→A) to Matrix m n A, with (i,j)-entry equal to v_i w_j.
Русский
Операция vecMulVec — билинейное отображение из (m→A) × (n→A) в Matrix m n A, с i,j-ой записью v_i w_j.
LaTeX
$$vecMulVecBilin : (m → A) →ₗ[R] (n → A) →ₗ[S] Matrix m n A$$
Lean4
/-- `vecMulVec` as a bilinear map.
When `A` is noncommutative, `R` and `S` can be instantiated as `vecMulVecLinear A Aᵐᵒᵖ`. -/
@[simps]
def vecMulVecBilin : (m → A) →ₗ[R] (n → A) →ₗ[S] Matrix m n A
where
toFun
x :=
{ toFun y := vecMulVec x y
map_add' _ _ := vecMulVec_add _ _ _
map_smul' _ _ := vecMulVec_smul _ _ _ }
map_add' _ _ := LinearMap.ext fun _ => add_vecMulVec _ _ _
map_smul' _ _ := LinearMap.ext fun _ => smul_vecMulVec _ _ _
