Commit 2024-09-11 14:35 5d603d75

feat(Algebra/BigOperators/Associated): add lemma divisor_closure_eq_closure (#11888) We add divisor_closure_eq_closure: Let x, y be elements of a CancelCommMonoidWithZero. If x * y can be written as a product of units and prime elements, then x can be written as a product of units and prime elements. We later use divisor_closure_eq_closure to prove Kaplansky's criterion (which we plan to add in a future PR).