map_circulant — Mathlib

English

Applying a map f to the entries of a circulant matrix yields a circulant matrix of the mapped entries: map f (circulant v) = circulant (λ i, f(v i)).

Русский

Применение отображения f к элементам Circulant-матрицы даёт Circulant-матрицу с образами элементов: map f (circulant v) = circulant (λ i, f(v i)).

LaTeX

$$$\\text{map}_{} f(\\text{circulant } v) = \\text{circulant}(\\lambda i. f(v(i)))$$$

Lean4

theorem map_circulant [Sub n] (v : n → α) (f : α → β) : (circulant v).map f = circulant fun i => f (v i) :=
  ext fun _ _ => rfl

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