circulant_smul — Mathlib

English

Scaling a circulant matrix by a scalar is the same as forming the circulant of the scaled generating vector: circulant(k · v) = k · circulant(v).

Русский

Умножение циркулянта на скаляр равно формированию циркулянта из масштабированного порождающего вектора: circulant(k·v) = k·circulant(v).

LaTeX

$$$\\operatorname{circulant}(k \\cdot v) = k \\cdot \\operatorname{circulant}(v)$$$

Lean4

/-- `k • circulant v` is another circulant matrix `circulant (k • v)`. -/
theorem circulant_smul [Sub n] [SMul R α] (k : R) (v : n → α) : circulant (k • v) = k • circulant v :=
  rfl

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