cons_sub_cons

Mathlib.Algebra.Group.Fin.Tuple

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

English

The difference of two vecCons vectors equals the vecCons of the coordinatewise differences.

Русский

Разность двух vecCons равна vecCons по координатам.

LaTeX

$$$ \mathrm{vecCons} x v - \mathrm{vecCons} y w = \mathrm{vecCons}(x - y) (v - w) $$$

Lean4

theorem cons_sub_cons (x : α) (v : Fin n → α) (y : α) (w : Fin n → α) :
    vecCons x v - vecCons y w = vecCons (x - y) (v - w) := by simp

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

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

Разделы

Аффилиация

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