Commit 2024-02-12 10:30 32a9a098

View on Github →

chore(Data/Finset/Basic): lemmas about toFinset (#10427)

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

added theorem List.toFinset_filter

added theorem List.toFinset_range

added theorem Multiset.toFinset_filter

added theorem Multiset.toFinset_range