Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-10 06:10 36fceb91

View on Github →

feat(data/list/cycle): Define cycle.chain analog to list.chain (#12970) We define cycle.chain, which means that a relation holds in all adjacent elements in a cyclic list. We then show that for r a transitive relation, cycle.chain r l is equivalent to r holding for all pairs of elements in l.

Estimated changes