Theorem Function.eq_update_self_iff

Modification history

2026-05-13 15:45
Mathlib/Logic/Function/Basic.lean
feat(Logic): declare optional simprocs for commuting equality and iff (#37850) …
Modified Function.eq_update_self_iffView on Github →
2022-11-10 23:55
Mathlib/Logic/Function/Basic.lean
feat(Logic/Function/Basic): `update_eq_self_iff` (#558) …
Added Function.eq_update_self_iffView on Github →