no goals
α : Type u_1
β : Type ?u.36269
m : Type ?u.36272
n : Type ?u.36275
R : Type ?u.36278
inst✝¹ : CommSemigroup α
inst✝ : AddCommMonoid α
⊢ ∀ (v w : Fin 0 → α), circulant v ⬝ circulant w = circulant w ⬝ circulant v
simp [Injective]