circulant_neg

Mathlib.LinearAlgebra.Matrix.Circulant

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

English

The circulant of minus a vector equals minus the circulant of the vector: circulant(-v) = -circulant(v).

Русский

Циркулярная матрица от минуса вектора равна минусу циркулярной матрицы от самого вектора.

LaTeX

$$$\\text{circulant}(-v) = -\\text{circulant}(v)$$$

Lean4

theorem circulant_neg [Neg α] [Sub n] (v : n → α) : circulant (-v) = -circulant v :=
  ext fun _ _ => rfl

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

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

Разделы

Аффилиация

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