English
The product of two circulant matrices circulant(v) and circulant(w) equals the circulant matrix generated by the vector circulant(v) *ᵥ w.
Русский
Произведение циркулярных матриц равняется циркулярной матрице, порожденной вектором circulant(v) *ᵥ w.
LaTeX
$$$\\operatorname{circulant}(v) \\cdot \\operatorname{circulant}(w) = \\operatorname{circulant}(\\operatorname{circulant}(v) *\\!\\!\\!_{\\mathrm{vec}} w)$$$
Lean4
/-- The product of two circulant matrices `circulant v` and `circulant w` is
the circulant matrix generated by `circulant v *ᵥ w`. -/
theorem circulant_mul [NonUnitalNonAssocSemiring α] [Fintype n] [AddGroup n] (v w : n → α) :
circulant v * circulant w = circulant (circulant v *ᵥ w) :=
by
ext i j
simp only [mul_apply, mulVec, circulant_apply, dotProduct]
refine Fintype.sum_equiv (Equiv.subRight j) _ _ ?_
intro x
simp only [Equiv.subRight_apply, sub_sub_sub_cancel_right]
