Commit 2024-12-03 19:01 da9df8db

View on Github →

feat: List.destutter on cotransitive relations. (#9082) List.destutter behaves nicely when the condition is a cotransitive relation, and even better when it's a coequivalence relation. This proves that behavior.

Estimated changes

Modified Mathlib/Data/List/Destutter.lean

added theorem List.Chain'.length_le_length_destutter

added theorem List.Chain'.length_le_length_destutter_ne

added theorem List.le_length_destutter'_cons

added theorem List.length_destutter'_congr

added theorem List.length_destutter'_cotrans_ge

added theorem List.length_destutter_le_length_destutter_cons

added theorem List.length_destutter_ne_le_length_destutter_cons

added theorem List.map_destutter

added theorem List.map_destutter_ne

Modified Mathlib/Data/List/GetD.lean

added theorem List.getD_replicate

added theorem List.getD_reverse

Modified Mathlib/Order/Basic.lean