circulant_col_zero_eq

Mathlib.LinearAlgebra.Matrix.Circulant

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

English

The circulant construction is injective: if Circulant(v) = Circulant(w) then v = w.

Русский

Конструкция циркулятова матрицы инъективна: если Circulant(v) = Circulant(w), то v = w.

LaTeX

$$Circulant injective: Circulant v = Circulant w ⇒ v = w$$

Lean4

theorem circulant_col_zero_eq [SubtractionMonoid n] (v : n → α) (i : n) : circulant v i 0 = v i :=
  congr_arg v (sub_zero _)

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

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

Разделы

Аффилиация

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