factorization): Lemma on zero-ness of factorization (#14560)

Commit

3 years ago

feat(data/nat/factorization): Lemma on zero-ness of factorization (#14560) Sad naming is sad. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author

Smaug123

Parents

043fa29d

mathlib3 736b4e5c - feat(data/nat/factorization): Lemma on zero-ness of factorization (#14560)

mathlib3
736b4e5c - feat(data/nat/factorization): Lemma on zero-ness of factorization (#14560)