Commit 2026-02-02 17:36 aaa0b3d3

View on Github →

refactor(RingTheory/UniqueFactorizationDomain/Basic): golf factors_pos (#34253) This PR golfs factors_pos by extracting two lemmas factors_of_isUnit and factors_eq_zero.

Estimated changes