neg_cons

Mathlib.Algebra.Group.Fin.Tuple

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

English

Let x ∈ α and v : Fin n → α. Then -vecCons x v = vecCons(-x) (-v).

Русский

Пусть x ∈ α и v : Fin n → α. Тогда -vecCons x v = vecCons(-x) (-v).

LaTeX

$$$-\\,\\operatorname{vecCons}(x,v) = \\operatorname{vecCons}(-x,-v)$$$

Lean4

@[simp]
theorem neg_cons (x : α) (v : Fin n → α) : -vecCons x v = vecCons (-x) (-v) := by ext i; refine i.cases ?_ ?_ <;> simp

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

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

Разделы

Аффилиация

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