mathlib

ac283c22 - feat(data/nat/prime): some lemmas about prime factors (#10385)

feat(data/nat/prime): some lemmas about prime factors (#10385) A few small lemmas about prime factors, for use in future PRs on prime factorisations and the Euler product formula for totient