[Merged by Bors] - feat(data/nat/factorization): Lemma on zero-ness of factorization

[Smaug123]

Sad naming is sad.

[Smaug123]

I'm not very well up on the naming conventions of mathlib, but factorization_apply_eq_zero_iff seems to me like the kind of thing I would only find indirectly by getting it wrong with a search for the string factorization_eq_zero, discovering the definition of factorization_eq_zero_iff, and then seeing that the lemma I wanted was the one immediately after it. If at all possible, I would prefer to keep factorization_eq_zero_iff as a substring, so that a text search will directly find the lemma.

[b-mehta]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests