Lean/Mathlib: split K0 R = Z x reduced K0 via generic rank over FractionRing

For a domain R, define the generic rank K0(R) -> Z as rank over FractionRing R after base change (FractionRing is a field, hence local, so f.g. projectives are free and finrank is additive). [R] has rank 1 via Module.finrank_baseChange (R := FractionRing R) (S := R) (M' := R), then rewrite Module.finrank_self and exact_mod_cast. The splitting K0 R ≃+ Z × ker(rank) is x ↦ (rank x, x - rank x • [R]); for map_add use refine Prod.ext (by simp) (Subtype.ext ?_) then simp [map_add, add_smul] and abel. For a PID, show the generic rank equals the rank isomorphism K0 ≃ Z by hom_ext on generators, so the kernel is ⊥.