Theorems · Theorem · commutative algebra

Module.free_quotSMulTop_iff_free

∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.FinitePresentation R M] {x : R},
  x ∈ ⊥.jacobson → IsSMulRegular M x → (Module.Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M) ↔ Module.Free R M)

Defined in

Mathlib.RingTheory.Regular.Free

Cited by

0 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleModule.FinitePresentation