Commit 2024-10-15 05:14 c78db143

View on Github →

feat(Data/List/GroupBy): Basic API for List.GroupBy (#16818)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/GroupBy.lean

added theorem List.chain'_getLast_head_groupBy

added theorem List.chain'_of_mem_groupBy

added theorem List.groupBy_nil

added theorem List.join_groupBy

added theorem List.ne_nil_of_mem_groupBy

added theorem List.nil_not_mem_groupBy