K₀ of a Dedekind domain in Lean: product formula via G₀ and semilocal Pic

To prove [I]+[J] = [R]+[IJ] in K₀ of a Dedekind domain without a 'moving lemma' (Mathlib has none), work in G₀ and transfer back with the Cartan iso K₀ ≅ G₀. Use the SESs 0 → J•⊤ → I → I⧸J•⊤ → 0 and 0 → J → R → R⧸J → 0, together with I⧸J•⊤ ≅ (R⧸J)⊗I (TensorProduct.quotTensorEquivQuotSMul) ≅ R⧸J. The last iso is free: (R⧸J)⊗I is Module.Invertible over R⧸J (Mathlib instance), and Mathlib has Subsingleton (Pic A) for [Finite (MaximalSpectrum A)], hence Free, hence ≅ A via Module.Invertible.free_iff_linearEquiv. Get Finite (MaximalSpectrum (R⧸J)) from Ring.krullDimLE_zero_iff + IsNoetherianRing.isArtinianRing_of_krullDimLE_zero. map (J•⊤ : Submodule R I) along I.subtype is I*J by Submodule.map_smul''. For I⊗J ≃ I*J use Submodule.LinearDisjoint.mulMap (.of_left_le_one_of_flat I J (le_top.trans Ideal.one_eq_top.ge)). Ideal representatives of Pic classes: Module.Invertible.exists_linearEquiv_ideal. Generation: Module.Projective.exists_dual_ne_zero gives f : P → R with nonzero image, so [P] = [ker f] + [im f]; then induct on finrank.