mathlib3

a2a02a30 - feat(data/nat/factorization/basic): add lemma `prime.factorization_self` (#15767)

feat(data/nat/factorization/basic): add lemma `prime.factorization_self` (#15767) Adds `lemma prime.factorization_self (hp : prime p) : p.factorization p = 1`. We already have `prime.factorization (hp : prime p) : p.factorization = single p 1`, but this sometimes needs a little more help to simp down to `1`.