A finite flat module M is locally free if rankAtStalk M is constant

theorem Module.bijective_of_surjective_of_rankAtStalk_eq {R : Type u_1} [CommRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [Module.Finite R M] [Flat R M] [AddCommGroup N] [Module R N] [Module.Finite R N] [Flat R N] {φ : M →ₗ[R] N} (hs : Function.Surjective ⇑φ) (h : ∀ (m : Ideal R) [inst : m.IsMaximal], rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk N { asIdeal := m, isPrime := ⋯ }) : Function.Bijective ⇑φ

theorem Module.Free.away_of_finite_of_flat_of_rankAtStalk_constant {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Finite R M] [Flat R M] (p : Ideal R) [p.IsPrime] (h : ∀ (m : Ideal R) [inst : m.IsMaximal], rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }) : ∃ a ∉ p, Free (Localization.Away a) (LocalizedModule.Away a M)

Let M be a finite flat R-module, p be a prime ideal of R. If rankAtStalk M is constant, then there exists a ∉ p such that M is free after localization away from a.