DefinitionDefinition: Literature-sourcedProof: Not applicableSession-authored (Fable 5 assisted)judge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The $p$ -primary component of a module over a domain

Definition

Let $R$ be an integral domain, let $M$ be an $R$ -module, and let $p \in R$ be irreducible (Irreducible and prime elements of an integral domain). The $p$ -primary component of $M$ is

$M [p^{\infty}] : = {m \in M : p^{k} m = 0 for some integer k \geq 1} .$

It is contained in the torsion subset $Tor (M)$ of Annihilators, torsion elements and the torsion subset of a module. That both sets are submodules, as their names require, is proved in Torsion elements and $p$ -primary elements form submodules over a domain ↗.

Depends on

Used by

Dependency tree · two levels

7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

K. Conrad, Modules over a PID, Sections 4-5 (standard reference, not scraped)
M. Brussel, Finitely Generated Modules over a PID, Section 3 (standard reference, not scraped)

The pp-primary component of a module over a domain