Mathlib v3 is deprecated. Go to Mathlib v4

Theorem associates.factor_set.prod_eq_zero_iff

Modification history

2021-10-23 14:30

src/ring_theory/unique_factorization_domain.lean

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

Added associates.factor_set.prod_eq_zero_iff View on Github →