Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_equiv.unique_factorization_monoid_iff

Modification history

2022-03-24 10:12
src/ring_theory/unique_factorization_domain.lean
feat(ring_theory/polynomial): mv_polynomial over UFD is UFD (#12866)
Added mul_equiv.unique_factorization_monoid_iffView on Github →