Commit 2024-11-20 11:43 b6fb044a

chore(RingTheory): split UniqueFactorizationDomain.lean (#19256) This PR splits the big file UniqueFactorizationDomain.lean into many smaller files:

• UniqueFactorizationDomain.Defs contains the definition of WfDvdMonoid, UniqueFactorizationMonoid and factors
• UniqueFactorizationDomain.Basic contains basic results on the previous definition such as the equivalence between UniqueFactorizationMonoid and the existence of prime factors
• UniqueFactorizationDomain.NormalizedFactors defines UniqueFactorizationMonoid.normalizedFactors and contains basic results. (Or should we merge it into Defs/Basic?)
• UniqueFactorizationDomain.FactorSet defines Associates.FactorSet and Associates.factors
• UniqueFactorizationDomain.Finite proves that elements of a UFM with finitely many units have finitely many divisors. (This could be moved to Basic.lean but I find it niche enough to deserve its own file.)
• UniqueFactorizationDomain.Finsupp defines UniqueFactorizationMonoid.factorization as a Finsupp version of factors
• UniqueFactorizationDomain.GCDMonoid defines a GCD on a UFM
• UniqueFactorizationDomain.Ideal shows UFDs satisfy the ascending chain condition on ideals
• UniqueFactorizationDomain.Multiplicative contains results on multiplicative properties and functions.
• UniqueFactorizationDomain.Multiplicity relates factors.count and multiplicity
• UniqueFactorizationDomain.Nat contains the UniqueFactorizationMonoid Nat instance