English
Let R be a commutative semiring and M, M₂, M₃ be modules over R. There is a canonical bilinear map vecEmpty₂: M →ₗ[R] M₂ →ₗ[R] Fin 0 → M₃, defined by toFun m := LinearMap.vecEmpty. This map is bilinear and factors through the zero-dimensional target Fin 0 → M₃; equivalently, it represents the zero bilinear map in this degenerate case.
Русский
Пусть R — коммутативная полугруппа, и M, M₂, M₃ — модули над R. Существует каноническое билинейное отображение vecEmpty₂: M →ₗ[R] M₂ →ₗ[R] Fin 0 → M₃, задающееся образом toFun m := LinearMap.vecEmpty. Это отображение билинейно и отображает в нулевую размерность целевого пространства Fin 0 → M₃; по сути, это нулевое билинейное отображение в данной ситуации.
LaTeX
$$$vecEmpty_2 : M \to M_2 \to \mathrm{Fin}_0 \to M_3$$$
Lean4
/-- The empty bilinear map defeq to `Matrix.vecEmpty` -/
@[simps]
def vecEmpty₂ : M →ₗ[R] M₂ →ₗ[R] Fin 0 → M₃
where
toFun _ := LinearMap.vecEmpty
map_add' _ _ := LinearMap.ext fun _ => Subsingleton.elim _ _
map_smul' _ _ := LinearMap.ext fun _ => Subsingleton.elim _ _
