Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-15 04:22 0cbfbabb

View on Github →

refactor(logic/function): inv_fun takes a nonempty instance instead of inhabited (#2148)

Estimated changes

modified theorem function.inv_fun_neg
modified theorem function.inv_fun_on_neg