Theorem UniqueFactorizationMonoid.factors_of_isUnit

Modification history

2026-02-02 17:36

Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean

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

Added UniqueFactorizationMonoid.factors_of_isUnit View on Github →