Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-21 03:12 b11b83b2

View on Github →

feat(data/list/basic): rotate a list (#542)

Estimated changes

Modified data/list/basic.lean

added theorem list.drop_all

added theorem list.drop_append_of_le_length

added theorem list.length_rotate'

added theorem list.length_rotate

added theorem list.nth_append

added theorem list.nth_concat_length:

added theorem list.nth_le_append

added theorem list.nth_le_repeat

added theorem list.nth_le_singleton

added theorem list.prod_rotate_eq_one_of_prod_eq_one

added theorem list.rotate'_cons_succ

added theorem list.rotate'_eq_take_append_drop

added theorem list.rotate'_length

added theorem list.rotate'_length_mul

added theorem list.rotate'_mod

added theorem list.rotate'_nil

added theorem list.rotate'_rotate'

added theorem list.rotate'_zero

added theorem list.rotate_cons_succ

added theorem list.rotate_eq_rotate'

added theorem list.rotate_eq_take_append_drop

added theorem list.rotate_length

added theorem list.rotate_length_mul

added theorem list.rotate_mod

added theorem list.rotate_nil

added theorem list.rotate_rotate

added theorem list.rotate_zero

modified theorem list.take_all

added theorem list.take_append_of_le_length

Modified data/list/defs.lean

added def list.rotate'

added def list.rotate

Modified data/nat/modeq.lean

added theorem list.nth_rotate

added theorem list.rotate_eq_self_iff_eq_repeat