Commit 2025-04-08 16:19 89ec70c5

View on Github →

chore(Data/Finset): deprecate Finset.fin (#23830)

Estimated changes

Modified Mathlib/Data/Finset/Fin.lean

modified theorem Finset.fin_map

modified theorem Finset.fin_mono

modified theorem Finset.mem_fin

Modified Mathlib/Order/Interval/Finset/Fin.lean