Theorem Associates.eq_of_prod_eq_prod

Modification history

2025-10-06 20:40
Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
chore(RingTheory): golf entire `smul_eq_zero_of_mem`, `hasEval`, `eq_of_prod_eq_prod` and `isIntegral_of_mem_ringOfIntegers` (#28487)
Deleted Associates.eq_of_prod_eq_prodView on Github →
2024-11-20 11:43
Mathlib/RingTheory/UniqueFactorizationDomain.lean
chore(RingTheory): split `UniqueFactorizationDomain.lean` (#19256) …
Modified Associates.eq_of_prod_eq_prodView on Github →
2023-03-21 09:26
Mathlib/RingTheory/UniqueFactorizationDomain.lean
feat: port RingTheory.UniqueFactorizationDomain (#3003)
Added Associates.eq_of_prod_eq_prodView on Github →