Commit 2021-10-24 22:52 942e60f7

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.