mathlib

de53f9c4 - feat(data/nat/factorization): add two convenience lemmas (#11543)

feat(data/nat/factorization): add two convenience lemmas (#11543) Adds convenience lemmas `prime_of_mem_factorization` and `pos_of_mem_factorization`. Also adds a different proof of `factorization_prod_pow_eq_self` that doesn't depend on `multiplicative_factorization` and so can appear earlier in the file.