circulant_single — Mathlib

English

A circulant matrix generated by a single scalar a at index 0 is a diagonal (scalar) matrix with a on the diagonal: circulant(Pi.single 0 a) = scalar n a.

Русский

Циркулянтная матрица, порожденная единицей в нулевом индексе и значением a, является диагональной матрицей с a на диагонали: circulant(Pi.single 0 a) = a I_n.

LaTeX

$$$\\operatorname{circulant}(\\Pi\\text{single }0\\ a) = \\operatorname{scalar}(n)\\,a = a I_n$$$

Lean4

@[simp]
theorem circulant_single (n) [Semiring α] [DecidableEq n] [AddGroup n] [Fintype n] (a : α) :
    circulant (Pi.single 0 a : n → α) = scalar n a := by
  ext i j
  simp [Pi.single_apply, diagonal_apply, sub_eq_zero]

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