circulant_mul_comm — Mathlib

English

For v,w: Fin n → α, circulant v and circulant w commute under the same commutative assumptions.

Русский

Для v,w: Fin n → α циркулянты встречаются как коммутирующиеся при тех же предположениях.

LaTeX

$$$\\operatorname{circulant}(v) \\cdot \\operatorname{circulant}(w) = \\operatorname{circulant}(w) \\cdot \\operatorname{circulant}(v)$$$

Lean4

theorem circulant_mul_comm [CommMagma α] [AddCommMonoid α] :
    ∀ {n} (v w : Fin n → α), circulant v * circulant w = circulant w * circulant v
  | 0 => by simp
  | _ + 1 => Matrix.circulant_mul_comm

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