circulant_isSymm_apply

Mathlib.LinearAlgebra.Matrix.Circulant

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

English

If matrix circulant v is symmetric, then v(-i) = v(i) for i in Fin n; this specializes the general IsSymm criterion to Fin.

Русский

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

LaTeX

$$∎$$

Lean4

theorem circulant_isSymm_apply {n} {v : Fin n → α} (h : (circulant v).IsSymm) (i : Fin n) : v (-i) = v i :=
  Fin.circulant_isSymm_iff.1 h i

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

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

Разделы

Аффилиация

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