Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.embedding.inv_of_mem_range_surjective

Modification history

2021-02-04 18:03
src/data/fintype/basic.lean
feat(data/fintype/basic): inv of inj on deceq (#5872)
Added function.embedding.inv_of_mem_range_surjectiveView on Github →