Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.injective.eq_iff

Modification history

2021-02-26 04:07
src/logic/function/basic.lean
fix(logic/{function}/basic): remove simp lemmas `function.injective.eq_iff` and `imp_iff_right` (#6402) …
Modified function.injective.eq_iffView on Github →
2017-12-20 23:25
logic/function.lean
refactor(data/ordinal): rearrange files, more cofinality
Modified function.injective.eq_iffView on Github →
2017-11-23 23:33
logic/function.lean
feat(data/finset): fintype, multiset.sort, list.pmap
Modified function.injective.eq_iffView on Github →
2017-10-15 01:58
logic/function.lean
feat(*): working on list/basic, robusting simp proofs
Added function.injective.eq_iffView on Github →