Commit 2020-08-16 11:27 a6f64343

feat(data/fin): bundled embedding (#3822) Add the coercion from fin n to ℕ as a bundled embedding, an equivalent of function.embedding.subtype. Once leanprover-community/lean#359 is fixed (making fin n a subtype), this can go away as a duplicate, but until then it is useful.