HepLean Documentation

Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain

Noetherian domains have unique factorization #

Main results #

IsNoetherianRing.wfDvdMonoid #

@[instance 100]
Equations
  • =