circulant_mul — Mathlib

English

For v,w: Fin n → α, the product circulant v · circulant w equals circulant of circulant v ·ᵥ w.

Русский

Для v, w: Fin n → α выполняется circulant v · circulant w = circulant( circulant v ·ᵥ w ).

LaTeX

$$$\\operatorname{circulant}(v) \\cdot \\operatorname{circulant}(w) = \\operatorname{circulant}(\\operatorname{circulant}(v) *\\!\\!\\mathrm{vec} w)$$$

Lean4

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

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