mathlib3

942e60f7 - chore(algebra/*/pi): add missing lemmas about function.update and set.piecewise (#9935)

chore(algebra/*/pi): add missing lemmas about function.update and set.piecewise (#9935) This adds `function.update_{zero,one,add,mul,sub,div,neg,inv,smul,vadd}`, and moves `pi.piecewise_{sub,div,neg,inv}` into the `set` namespace to match `set.piecewise_{add,mul}`. This also adds `finset.piecewise_erase_univ`, as this is tangentially related.