Commit 2025-02-12 22:31 3b1a275d

View on Github →

feat(List/Count): add countP_lt_length_iff (#21774) ... and count_lt_length_iff. Also use variables for implicit arguments.

Estimated changes

modified theorem List.countP_diff
modified theorem List.countP_erase
modified theorem List.count_diff
modified theorem List.count_map_of_injective