Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-02-02 14:43
508c2650
View on Github →
feat(logic/function/basic): add bijective.iff_exists_unique and projections (
#5995
)
Estimated changes
Modified
src/logic/function/basic.lean
added
theorem
function.bijective.exists_unique
added
theorem
function.bijective_iff_exists_unique