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

Equations

• ⋯ = ⋯