Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-15 13:05 bf6eeb24

View on Github →

feat(data/list/cycle): cycle.map and has_repr (#8170)

Estimated changes

Modified src/data/list/cycle.lean

added def cycle.lists

added def cycle.map

added theorem cycle.mem_lists_iff_coe_eq

Modified src/data/list/rotate.lean

added theorem list.is_rotated.map

added theorem list.map_rotate

Created test/cycle.lean