Mathlib v3 is deprecated. Go to Mathlib v4

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 :=

Estimated changes