theorem SerreAffineCriterion.serre_localization_flat (R : Type u_1) [CommRing R] (S : Submonoid R) : Module.Flat R (Localization S)

Localization at a submonoid S ⊆ R produces a flat R-module, a key input for Serre's affineness criterion (exactness of global sections on affine opens).