circulant_apply

Mathlib.LinearAlgebra.Matrix.Circulant

URI: https://scilib.ai/kg/mathlib#Matrix.circulant_apply

Lean4

@[simp]
theorem circulant_apply [Sub n] (v : n → α) (i j) : circulant v i j = v (i - j) :=
  rfl

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

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

Разделы

Аффилиация

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