mathlib3

8ad70779 - feat(data/nat/factorization/basic): lemmas about `n.factorization p = 0` (#16185)

feat(data/nat/factorization/basic): lemmas about `n.factorization p = 0` (#16185) Adds some lemmas characterising conditions when `n.factorization p = 0`. This PR also rearranges the order of some lemmas to better group them together (and adds some section docstrings). Also swaps the names `factorization_eq_zero_iff` and `factorization_eq_zero_iff'`.