mathlib
60cb2cfe - feat(data/list): length_filter_lt_length_iff_exists (#10074)

Commit

4 years ago

feat(data/list): length_filter_lt_length_iff_exists (#10074) Also moved a lemma about filter_map that was placed in the wrong file

Author

TwoFX

Parents