mathlib
0a8e3eda - feat(data/equiv/fin): fin_order_iso_subtype (#8258)

Commit
4 years ago
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`. Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Author
Parents
Loading