no goals
α : Type u_1
β : Type ?u.64581
m : Type ?u.64584
n : Type ?u.64587
R : Type ?u.64590
v✝ : Fin 0 → α
⊢ IsSymm (circulant v✝) ↔ ∀ (i : Fin 0), v✝ (-i) = v✝ i
simp [IsSymm.ext_iff, IsEmpty.forall_iff]