Theorems · Theorem · commutative algebra

Submodule.exists_isInternal_prime_power_torsion

∀ {R : Type u} [inst : CommRing R] [IsDedekindDomain R] {M : Type v} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.Finite R M],
  Module.IsTorsion R M →
    ∃ P x, ∃ (_ : ∀ p ∈ P, Prime p), ∃ e, DirectSum.IsInternal fun p => Submodule.torsionBySet R M ↑(↑p ^ e p)

A finitely generated torsion module over a Dedekind domain is an internal direct sum of its p i ^ e i-torsion submodules for some prime ideals p i and numbers e i.

Defined in

Mathlib.Algebra.Module.DedekindDomain

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainAddCommGroupModuleModule.Finite