Theorem UniqueFactorizationMonoid.factors_eq_zero

Modification history

2026-02-02 17:36

Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean

refactor(RingTheory/UniqueFactorizationDomain/Basic): golf `factors_pos` (#34253) …

Added UniqueFactorizationMonoid.factors_eq_zero View on Github →