English
The circulant matrix built from the function that is 1 at 0 and 0 elsewhere is the identity; more generally, circulant(ite(i = 0,1,0)) = I_d.
Русский
Циркулянтная матрица, построенная из функции, которая равна 1 только в нуле, является единичной; в общем случае circulant(ite(i = 0,1,0)) = I.
LaTeX
$$$\\operatorname{circulant}(\\text{fun } i \\mapsto \\text{ite}(i.1 = 0, 1, 0)) = I_n$$$
Lean4
/-- Note we use `↑i = 0` instead of `i = 0` as `Fin 0` has no `0`.
This means that we cannot state this with `Pi.single` as we did with `Matrix.circulant_single`. -/
theorem circulant_ite (α) [Zero α] [One α] : ∀ n, circulant (fun i => ite (i.1 = 0) 1 0 : Fin n → α) = 1
| 0 => by simp [eq_iff_true_of_subsingleton]
| n + 1 => by
rw [← circulant_single_one]
congr with j
simp [Pi.single_apply]
