Theorems · Theorem · commutative algebra

Submodule.isInternal_prime_power_torsion

∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {M : Type v} [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.Finite R M],
  Module.IsTorsion R M →
    DirectSum.IsInternal fun p =>
      Submodule.torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors ⊤.annihilator))

A finitely generated torsion module over a Dedekind domain is an internal direct sum of its p i ^ e i-torsion submodules where p i are factors of (⊤ : Submodule R M).annihilator and e i are their multiplicities.

Defined in

Mathlib.Algebra.Module.DedekindDomain

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainAddCommGroupModuleModule.Finite