Theorems · Theorem · commutative algebra

Ideal.torsionOf_eq_span_pow_pOrder

∀ {R : Type u} [inst : CommRing R] [IsPrincipalIdealRing R] {M : Type v} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [IsDomain R] {p : R},
  Irreducible p →
    ∀ (hM : Module.IsTorsion' M ↥(Submonoid.powers p)) [dec : (x : M) → Decidable (x = 0)] (x : M),
      Ideal.torsionOf R M x = Ideal.span {p ^ Submodule.pOrder hM x}

Defined in

Mathlib.Algebra.Module.PID

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsPrincipalIdealRingAddCommGroupModuleIsDomainDecidable