vecEmpty_apply

Mathlib.LinearAlgebra.Pi

URI: https://scilib.ai/kg/mathlib#LinearMap.vecEmpty_apply

English

The evaluation of vecEmpty at m equals the zero vector in Matrix.vecEmpty.

Русский

Значение vecEmpty в m равно нулевому вектору Matrix.vecEmpty.

LaTeX

$$$$ vecEmpty(m) = \\text{Matrix.vecEmpty}, $$$$

Lean4

@[simp]
theorem vecEmpty_apply (m : M) : (LinearMap.vecEmpty : M →ₗ[R] Fin 0 → M₃) m = ![] :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru