mathlib3
90abd3bb - feat(data/fintype): finset.univ_map_embedding (#2765)

Commit
5 years ago
feat(data/fintype): finset.univ_map_embedding (#2765) Adds the lemma ``` lemma finset.univ_map_embedding {α : Type*} [fintype α] (e : α ↪ α) : (finset.univ).map e = finset.univ := ``` Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Author
Parents
Loading