Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-23 14:30 95535a3e

View on Github →

refactor(ring_theory/unique_factorization_domain): golf some factor_set lemmas (#9889)

Estimated changes

Modified src/ring_theory/unique_factorization_domain.lean

added theorem associates.factor_set.prod_eq_zero_iff

added theorem associates.factor_set.unique

modified theorem associates.factors'_cong

modified theorem associates.prod_factors