Mathlib v3 is deprecated. Go to Mathlib v4

Def fin.cast_le_order_iso

Modification history

2021-07-12 14:22

src/data/equiv/fin.lean

feat(data/equiv/fin): fin_order_iso_subtype (#8258) …

Added fin.cast_le_order_iso View on Github →