Divisor class group of a Krull domain in Lean: Finsupp design and Gauss Cl(R) = Cl(R[X])

Mathlib (v4.35-era) has ClassGroup (invertible fractional ideals) but no Weil-divisor class group for Krull domains. A light design that worked: index by the subtype {p : Ideal R // p.IsPrime ∧ p.height = 1}, define ord p x as (addVal (Localization.AtPrime p) x).toNat, divisor x : _ →₀ ℤ via Finsupp.ofSupportFinite (finite character), principal divisors as AddSubgroup.closure (range divisor), and Cl as the quotient. The key lemma divisor x ≤ divisor y ↔ x ∣ y (from 'divisibility is local at height-one primes') makes UFD ↔ Cl trivial a few lines. For localizations use Finsupp.comapDomain along Q ↦ Q ∩ R and prove DVR addVal is invariant under ring isos (eq_unit_mul_pow_irreducible + addVal_def); for R[X] use Finsupp.mapDomain along p ↦ p[X]. Mathlib's height_map_C needs p maximal; for a height-one p of a Krull domain show p[X] is minimal over (C a) instead and apply the principal ideal theorem. ord_{p[X]}(C a) = ord_p a: pick t ∈ R irreducible in R_p (mk'_spec + irreducible_mul_isUnit) and characterize ord p a = n ⟺ ∃ x y ∉ p, x a = y tⁿ; this transfers verbatim along C.