Commit 2022-11-10 23:55 4680538b

View on Github →

feat(Logic/Function/Basic): update_eq_self_iff (#558) Matches https://github.com/leanprover-community/mathlib/pull/17168 I do not have access to non-master branches so this PR is from a fork.

Estimated changes

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.eq_update_self_iff

added theorem Function.ne_update_self_iff

added theorem Function.update_eq_self_iff

added theorem Function.update_ne_self_iff