English
Given a function v: n → α, the circulant matrix Circulant(v) has entries (Circulant(v))_{i j} = v(i − j).
Русский
Для функции v: n → α, циркулярная матрица Circulant(v) имеет элементы (Circulant(v))_{i j} = v(i − j).
LaTeX
$$[Sub n] (v : n → α) : Circulant v_{i j} = v(i - j)$$
Lean4
/-- Given the condition `[Sub n]` and a vector `v : n → α`,
we define `circulant v` to be the circulant matrix generated by `v` of type `Matrix n n α`.
The `(i,j)`th entry is defined to be `v (i - j)`. -/
def circulant [Sub n] (v : n → α) : Matrix n n α :=
of fun i j =>
v
(i - j)
-- TODO: set as an equation lemma for `circulant`, see https://github.com/leanprover-community/mathlib4/pull/3024
