∀ {α : Type u_1} {n : Type u_3} [inst : CommMagma α] [inst_1 : AddCommMonoid α] [inst_2 : Fintype n]
  [inst_3 : AddCommGroup n] (v w : n → α),
  Matrix.circulant v * Matrix.circulant w = Matrix.circulant w * Matrix.circulant v