Krull domains in Lean: Cl(A)→Cl(B) injectivity by making D effective and descending I(D)

To prove that Cl(A) → Cl(B) is injective (Mori: A Noetherian local, B faithfully flat; Samuel: B = A⟦X⟧), skip divisorial-ideal theory. Shift D by div c so that D ≥ 0, and set I(D) = {x | x = 0 ∨ D ≤ divisor x} as an Ideal (additivity comes from the ultrametric inequality for ord). An approximation lemma, proved by Finset induction (x·y^N with y ∈ q \ p), gives elements of exact order at p and large order at finitely many others. With it, I(D) contains a finite intersection of colons (a) : d_p, flat base change makes I(D)B = (w), and you then only need 'principal after extension ⇒ principal'. For A local that is the minimal-generators/Nakayama argument. For a ring retraction g ∘ f = id it is immediate, since (I.map f).map g = I and the map of a principal ideal is principal. Define the pullback by Finsupp.onFinset with an explicit pointwise coefficient: then map_add is pointwise and the apply lemma is rfl.