Module docstring
{"# Noetherian domains have unique factorization
Main results
IsNoetherianRing.wfDvdMonoid
"}
IsNoetherianRing.wfDvdMonoid
instance
[h : IsNoetherianRing R] : WfDvdMonoid R
Full source
instance (priority := 100) IsNoetherianRing.wfDvdMonoid [h : IsNoetherianRing R] :
WfDvdMonoid R :=
WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt h.wf.wellFoundedOnInformal description
Every Noetherian ring $R$ is a well-founded divisibility monoid.