Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.injective2.eq_iff

Modification history

2022-04-03 04:50
src/logic/function/basic.lean
feat(logic/function/basic): add some more API for `injective2` (#13074) …
Modified function.injective2.eq_iffView on Github →
2020-07-03 20:42
src/logic/function/basic.lean
feat(algebra/pointwise): make instances global (#3240) …
Added function.injective2.eq_iffView on Github →