Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.embedding.right_inv_of_inv_of_mem_range

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.right_inv_of_inv_of_mem_rangeView on Github →