Commit 2023-01-13 05:43 527e406f
View on Github →chore(data/list): golf, merge 2 files (#18120)
- merge
data.list.modeqintodata.list.rotate; - mark
list.rotate_eq_rotateas@[simp]; - golf some proofs.
chore(data/list): golf, merge 2 files (#18120)
data.list.modeq into data.list.rotate;list.rotate_eq_rotate as @[simp];