Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-12 14:22 0a8e3eda

View on Github →

feat(data/equiv/fin): fin_order_iso_subtype (#8258) Promote a fin n into a larger fin m, as a subtype where the underlying values are retained. This is the order_iso version of fin.cast_le.

Estimated changes