circulant_zero — Mathlib

English

Let α be a type with a zero element. The circulant matrix generated by the zero function is the zero matrix: circulant 0 = 0.

Русский

Пусть α — тип с нулевым элементом. Циркулярная матрица, порожденная нулевой функцией, равна нулевой матрице: circulant 0 = 0.

LaTeX

$$$\\operatorname{circulant}(0) = 0_{\,n\\times n}\\,,$$$

Lean4

@[simp]
theorem circulant_zero (α n) [Zero α] [Sub n] : circulant 0 = (0 : Matrix n n α) :=
  ext fun _ _ => rfl

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