circulant_isSymm_iff

Mathlib.LinearAlgebra.Matrix.Circulant

URI: https://scilib.ai/kg/mathlib#Matrix.Fin.circulant_isSymm_iff

← MathLib Explorer

English

If circulant v is symmetric, then v(-i) = v(i) for all i in Fin n.

Русский

Если circulant v симметрична, то для каждого i в Fin n выполняется v(-i) = v(i).

LaTeX

$${\n ...\n}$$

Lean4

theorem circulant_isSymm_iff : ∀ {n} {v : Fin n → α}, (circulant v).IsSymm ↔ ∀ i, v (-i) = v i
  | 0 => by simp [IsSymm.ext_iff, IsEmpty.forall_iff]
  | _ + 1 => Matrix.circulant_isSymm_iff

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru