Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-11 18:25 7c523cb7

View on Github →

feat(data/list/count): partially sync with multiset (#18125)

  • rename list.count_repeat to list.count_repeat_self;
  • prove list.count_repeat with if .. then .. else in the RHS.

Estimated changes