← Mathematical handbook

Noetherian domains have unique factorization

Main results

• IsNoetherianRing.wfDvdMonoid

@[instance 100]

instance IsNoetherianRing.wfDvdMonoid {R : Type u_1} [CommSemiring R] [IsDomain R] [h : IsNoetherianRing R] : WfDvdMonoid R