Commit 2023-04-23 09:27 8bc7aecb

View on Github →

feat: Function.update is monotone (#3587) Match leanprover-community/mathlib#6418 and leanprover-community/mathlib#18841

Estimated changes

added theorem Pi.mulSingle_mono
added theorem Pi.single_mul_left
added theorem Pi.single_mul_right
added theorem update_le_update_iff'
added theorem update_lt_update_iff
added theorem Function.update_mono