circulant_add — Mathlib

English

Circulant is additive with respect to the generating vector: 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_add [Add α] [Sub n] (v w : n → α) : circulant (v + w) = circulant v + circulant w :=
  ext fun _ _ => rfl

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