neg_empty

Mathlib.Algebra.Group.Fin.Tuple

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

English

The negation of an empty vector is the empty vector.

Русский

Отрицание пустого вектора равно пустому вектору.

LaTeX

$$$ -v = \vecEmpty $$$

Lean4

@[simp]
theorem neg_empty (v : Fin 0 → α) : -v = ![] :=
  empty_eq _

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

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

Разделы

Аффилиация

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