Theorem WfDvdMonoid.exists_factors

Modification history

2023-03-21 09:26

Mathlib/RingTheory/UniqueFactorizationDomain.lean

feat: port RingTheory.UniqueFactorizationDomain (#3003)

Added WfDvdMonoid.exists_factors View on Github →