Freeness of QuotSMulTop by a regular element

Let M be a finitely presented module over a commutative ring R. If x is in the Jacobson radical of R and x is M-regular, then M/xM is free over R/(x) if and only if M is free over R.

instance instFreeQuotientIdealSpanSingletonSetQuotSMulTop (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Free R M] (x : R) : Module.Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)

theorem Module.free_quotSMulTop_iff_free (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [FinitePresentation R M] {x : R} (mem : x ∈ ⊥.jacobson) (reg : IsSMulRegular M x) : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M) ↔ Free R M