English
Applying the isomorphism intSpanEquivQuotAddOrderOf to the pair ⟨a, mem_span_singleton_self a⟩ yields the quotient class of 1.
Русский
Применяя изоморфизм intSpanEquivQuotAddOrderOf к ⟨a, mem_span_singleton_self a⟩, получаем класс 1 в фактор-модуле.
LaTeX
$$$intSpanEquivQuotAddOrderOf a (\langle a, Submodule.mem_span_singleton_self a \rangle) = Submodule.Quotient.mk 1$$$
Lean4
/-- 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. -/
theorem isInternal_prime_power_torsion [DecidableEq (Ideal R)] [Module.Finite R M] (hM : Module.IsTorsion R M) :
DirectSum.IsInternal fun p : (factors (⊤ : Submodule R M).annihilator).toFinset =>
torsionBySet R M (p ^ (factors (⊤ : Submodule R M).annihilator).count ↑p : Ideal R) :=
by
have hM' := Module.isTorsionBySet_annihilator_top R M
have hI := Submodule.annihilator_top_inter_nonZeroDivisors hM
refine isInternal_prime_power_torsion_of_is_torsion_by_ideal ?_ hM'
rw [← Set.nonempty_iff_ne_empty] at hI; rw [Submodule.ne_bot_iff]
obtain ⟨x, H, hx⟩ := hI; exact ⟨x, H, nonZeroDivisors.ne_zero hx⟩
