Commit 2022-08-29 11:13 8ad70779

View on Github →

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'.

Estimated changes

Modified src/data/nat/factorization/basic.lean

modified theorem nat.factorization_eq_zero_iff'

modified theorem nat.factorization_eq_zero_iff

added theorem nat.factorization_eq_zero_iff_remainder

added theorem nat.factorization_eq_zero_of_not_dvd

added theorem nat.factorization_eq_zero_of_remainder

added theorem nat.prime.eq_of_factorization_pos