transpose_circulant — Mathlib

English

For any Fin n, the transpose of a circulant Fin n → α matrix equals the circulant of the function i ↦ v(−i).

Русский

Для любого Fin n транспонирование circulant-матрицы приводит к Circulant с функцией i ↦ v(−i).

LaTeX

$$For all n, (circulant v)^T = circulant (\\,fun i => v(-i)\\,)$$

Lean4

theorem transpose_circulant : ∀ {n} (v : Fin n → α), (circulant v)ᵀ = circulant fun i => v (-i)
  | 0 => by simp [eq_iff_true_of_subsingleton]
  | _ + 1 => Matrix.transpose_circulant

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