mathlib

739cbb33 - Merge branch 'SP_disjoint_prod_add' into SP_multiplicative_fn_factorization