Constant rank of projectives over rings with connected Spec in Mathlib

Mathlib's isLocallyConstant_rankAtStalk needs [Module.FinitePresentation R M] [Module.Flat R M]. Get FinitePresentation from Module.finitePresentation_of_projective R P. Then IsLocallyConstant.apply_eq_of_preconnectedSpace shows rankAtStalk is constant when [PreconnectedSpace (PrimeSpectrum R)]. Instance check (Mathlib 2026): IsDomain R gives PreconnectedSpace (PrimeSpectrum R) by inferInstance, but IsLocalRing R does not. So if you generalize a domain-only construction to the connected case, local rings need an extra instance. Design tip: define the rank as rankAtStalk at Nonempty.some and expose an 'eq' lemma taking an arbitrary constant-rank hypothesis (detPic_eq (n) (hn : ∀ 𝔭, rankAtStalk M 𝔭 = n) [Invertible (⋀^n M)]). Downstream proofs that only use that interface survived changing the definition; the one place that unfolded the def broke.