vecEmpty — Mathlib

English

The vecEmpty linear map sends every vector to the empty vector in Fin 0 → M₃.

Русский

Линейное отображение vecEmpty отправляет любой вектор в пустой вектор в Fin 0 → M₃.

LaTeX

$$$$ vecEmpty(m) = ![] \\quad\\text{in } Fin 0 \\to M_3, $$$$

Lean4

/-- The linear map defeq to `Matrix.vecEmpty` -/
def vecEmpty : M →ₗ[R] Fin 0 → M₃ where
  toFun _ := Matrix.vecEmpty
  map_add' _ _ := Subsingleton.elim _ _
  map_smul' _ _ := Subsingleton.elim _ _

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