circulant_isSymm_iff — Mathlib

English

A circulant matrix is symmetric iff its generating vector is invariant under negation, i.e., v(-i) = v(i) for all i.

Русский

Циркулярная матрица симметрична тогда и только тогда, когда порождающий вектор не меняется при отрицании: v(-i) = v(i) для всех i.

LaTeX

$$[SubtractionMonoid n] {v : n → α} : (circulant v).IsSymm ↔ ∀ i, v(-i) = v(i)$$

Lean4

/-- A circulant of `v` is symmetric iff `v` equals its reverse. -/
theorem circulant_isSymm_iff [SubtractionMonoid n] {v : n → α} : (circulant v).IsSymm ↔ ∀ i, v (-i) = v i := by
  rw [IsSymm, transpose_circulant, circulant_inj, funext_iff]

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