Commit 2024-10-30 23:50 2959869c

View on Github →

feat(Data/List/Chain): chain'_attachWith (#18429)

Estimated changes

Modified Mathlib/Data/List/Chain.lean

added theorem List.chain'_attach

added theorem List.chain'_attachWith