Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.injective.ne_iff'

Modification history

2020-07-06 05:41
src/logic/function/basic.lean
refactor(algebra/inj_surj): more lemmas, move to files, rename (#3290) …
Added function.injective.ne_iff'View on Github →