Commit 2024-10-07 11:43 fcafb6da

View on Github →

feat(Data/List/Chain): lemmas on Chain' and replicate (#17106)

Estimated changes

Modified Mathlib/Data/List/Chain.lean

added theorem List.chain'_eq_iff_eq_replicate

added theorem List.chain'_replicate_of_rel

added theorem List.chain_eq_iff_eq_replicate

added theorem List.chain_replicate_of_rel