Commit 2022-01-18 20:38 de53f9c4

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.