no goals
α : Type u_2
β : Type ?u.64028
m : Type ?u.64031
n : Type u_1
R : Type ?u.64037
inst✝ : AddGroup n
v : n → α
⊢ IsSymm (circulant v) ↔ ∀ (i : n), v (-i) = v i
rw [IsSymm, transpose_circulant, circulant_inj, funext_iff]