smul_empty

Mathlib.Algebra.Group.Fin.Tuple

URI: https://scilib.ai/kg/mathlib#Matrix.smul_empty

English

Any scalar action on an empty coordinate vector yields the empty vector.

Русский

Любое скалярное действие на пустой вектор координат даёт пустой вектор.

LaTeX

$$$ x \cdot v = \vecEmpty $$$

Lean4

@[simp]
theorem smul_empty (x : M) (v : Fin 0 → α) : x • v = ![] :=
  empty_eq _

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

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

Разделы

Аффилиация

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