conjTranspose_circulant — Mathlib

English

The conjugate transpose of a circulant matrix is circulant with the conjugate of the negated index: (circulant v)^H = circulant (star (fun i => v(-i))).

Русский

Сопряжено-транспонированная Circulant-матрица равна Circulant, взятой по звездообразному индексу: (circulant v)^H = circulant (звезда(функция i => v(-i))).

LaTeX

$$(circulant v)^H = circulant (star (fun i => v(-i)))$$

Lean4

theorem conjTranspose_circulant [Star α] [SubtractionMonoid n] (v : n → α) :
    (circulant v)ᴴ = circulant (star fun i => v (-i)) := by ext; simp

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