English
Multiplication of circulants commutes when the underlying algebra is commutative.
Русский
Умножение циркулянтов коммуutативно, если база коммутативна.
LaTeX
$$$\\operatorname{circulant}(v) \\cdot \\operatorname{circulant}(w) = \\operatorname{circulant}(w) \\cdot \\operatorname{circulant}(v)$$$
Lean4
/-- Multiplication of circulant matrices commutes when the elements do. -/
theorem circulant_mul_comm [CommMagma α] [AddCommMonoid α] [Fintype n] [AddCommGroup n] (v w : n → α) :
circulant v * circulant w = circulant w * circulant v :=
by
ext i j
simp only [mul_apply, circulant_apply]
refine Fintype.sum_equiv ((Equiv.subLeft i).trans (Equiv.addRight j)) _ _ ?_
intro x
simp only [Equiv.trans_apply, Equiv.subLeft_apply, Equiv.coe_addRight, add_sub_cancel_right, mul_comm]
congr 2
abel
