α : Type u
l✝ l' l : List α
h : cyclicPermutations l = [[]]
⊢ l = []
α : Type u
l✝ l' l : List α
⊢ cyclicPermutations l = [[]] ↔ l = []
refine' ⟨fun h => _, fun h => by simp [h]⟩
no goals
α : Type u
l✝ l' l : List α
h : cyclicPermutations l = [[]]
⊢ l = []
rw [eq_comm, ← isRotated_nil_iff', ← mem_cyclicPermutations_iff, h, mem_singleton]
no goals
α : Type u
l✝ l' l : List α
h : l = []
⊢ cyclicPermutations l = [[]]
simp [h]