Commit 2020-05-23 09:33 90abd3bb
View on Github →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 :=
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 :=