Mathlib v3 is deprecated. Go to Mathlib v4

Theorem wf_dvd_monoid.not_unit_iff_exists_factors_eq

Modification history

2022-04-29 22:22
src/ring_theory/unique_factorization_domain.lean
feat(ring_theory): factorize a non-unit into irreducible factors without multiplying a unit (#13682) …
Added wf_dvd_monoid.not_unit_iff_exists_factors_eqView on Github →