circulant_sub

Mathlib.LinearAlgebra.Matrix.Circulant

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

English

Circulant respects subtraction: circulant(v - w) = circulant(v) - circulant(w).

Русский

Циркулянт сохраняет вычитание: circulant(v - w) = circulant(v) - circulant(w).

LaTeX

$$$\\operatorname{circulant}(v - w) = \\operatorname{circulant}(v) - \\operatorname{circulant}(w)$$$

Lean4

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

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

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

Разделы

Аффилиация

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