mathlib

e86edfeb - Add docstring to `factorization_mul_of_pos`