Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.injective.inv_fun_restrict

Modification history

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