Commit 2023-03-26 23:21 c001e380

View on Github →

chore: sync Data.List.Rotate (#3040)

data.list.rotate@ccad6d5093bd2f5c6ca621fc74674cce51355af6..f694c7dead66f5d4c80f446c796a5aad14707f0e Also add non-deprecated versions of some lemmas (use List.get instead of List.nthLe).

Estimated changes

Modified Mathlib/Data/List/Rotate.lean

added theorem List.get?_rotate

added theorem List.get_eq_get_rotate

added theorem List.get_rotate

added theorem List.head?_rotate

added theorem List.rotate_eq_self_iff_eq_replicate

added theorem List.rotate_one_eq_self_iff_eq_replicate

added theorem List.rotate_replicate

modified theorem List.rotate_singleton