Theorem List.Chain'.iterate_eq_of_apply_eq

Modification history

2025-09-24 16:53

Mathlib/Data/List/Chain.lean

fix: adaptations for batteries#1421 (#29928) …

Deleted List.Chain'.iterate_eq_of_apply_eq View on Github →

2024-09-02 00:34

Mathlib/Data/List/Chain.lean

feat(Data/List/Change): add forwards induction for List.Chain and List.Chain' (#16346) …

Added List.Chain'.iterate_eq_of_apply_eq View on Github →