Commit 2023-09-20 16:02 96a11c7a

View on Github →

feat: add Function.update_eq_const and eq_const_of_subsingleton (#7275) Also golf Function.update_apply.

Estimated changes

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.update_eq_const_of_subsingleton

Modified Mathlib/Logic/Unique.lean

added theorem eq_const_of_subsingleton

modified theorem eq_const_of_unique