conjTranspose_circulant — Mathlib

English

For a Fin-n indexed vector, the conjTranspose of the circulant equals the circulant of the starred negated index.

Русский

Для вектора с индексами Fin n коньюгированно-транспонированная Circulant равно Circulant со звездообразованным отрицательным индексом.

LaTeX

$$(circulant v)^H = circulant (Pi.instStarForall.star (fun i => v ((Fin.neg n).neg i)))$$

Lean4

theorem conjTranspose_circulant [Star α] : ∀ {n} (v : Fin n → α), (circulant v)ᴴ = circulant (star fun i => v (-i))
  | 0 => by simp [eq_iff_true_of_subsingleton]
  | _ + 1 => Matrix.conjTranspose_circulant

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