Commit 2022-04-29 22:22 a70166a3
View on Github →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. Also removes some extraneous namespace prefix.