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