mathlib

a70166a3 - feat(ring_theory): factorize a non-unit into irreducible factors without multiplying a unit (#13682)

feat(ring_theory): factorize a non-unit into irreducible factors without multiplying a unit (#13682) Used in https://proofassistants.stackexchange.com/a/1312/93. Also adds simp lemma `multiset.prod_erase` used in the main proof and the auto-generated additive version, which is immediately analogous to [list.prod_erase](https://leanprover-community.github.io/mathlib_docs/data/list/big_operators.html#list.prod_erase). Also removes some extraneous namespace prefix.