Theorem WfDvdMonoid.not_isUnit_iff_exists_factors_eq

Modification history

2026-08-03 08:56
Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean
chore: rename a lemma containing `not_unit` (#42387)
Added WfDvdMonoid.not_isUnit_iff_exists_factors_eqView on Github →