Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.inv_fun_eq

Modification history

2021-11-29 17:49

src/logic/function/basic.lean

chore(logic/function): allow `Sort*` in `function.inv_fun` (#10526)

Modified function.inv_fun_eq View on Github →

2017-10-15 01:58

logic/function.lean

feat(*): working on list/basic, robusting simp proofs

Added function.inv_fun_eq View on Github →