Skip to content

Commit

Permalink
chore(Data/List/Rotate): add @[simp] to rotate_replicate (#10106)
Browse files Browse the repository at this point in the history
  • Loading branch information
s1m7u committed Jan 29, 2024
1 parent 89f9777 commit d883f18
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Data/List/Rotate.lean
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@ theorem length_rotate (l : List α) (n : ℕ) : (l.rotate n).length = l.length :
rw [rotate_eq_rotate', length_rotate']
#align list.length_rotate List.length_rotate

-- porting note: todo: add `@[simp]`
@[simp]
theorem rotate_replicate (a : α) (n : ℕ) (k : ℕ) : (replicate n a).rotate k = replicate n a :=
eq_replicate.2by rw [length_rotate, length_replicate], fun b hb =>
eq_of_mem_replicate <| mem_rotate.1 hb⟩
Expand Down

0 comments on commit d883f18

Please sign in to comment.