English
There exist a finite family of prime power torsion submodules giving an internal direct sum decomposition of M, indexed by a finite type with DecidableEq.
Русский
Существуют конечная семейство torsionBy по простым степеням и внутреннее разложение M в прямую сумму индексы которого имеют конечный тип иDecidableEq.
LaTeX
$$$\\exists ι (\\text{finite}) (p:ι \\to R) (\\forall i, Irreducible (p i)) (e:ι \\to \\mathbb{N}),\\ DirectSum.IsInternal (\\lambda i:ι,\\; \\mathrm{torsionBy}\\ R M (p i)^{e i})$$$
Lean4
theorem _root_.Ideal.torsionOf_eq_span_pow_pOrder (x : M) : torsionOf R M x = span {p ^ pOrder hM x} := by
classical
dsimp only [pOrder]
rw [← (torsionOf R M x).span_singleton_generator, Ideal.span_singleton_eq_span_singleton, ←
Associates.mk_eq_mk_iff_associated, Associates.mk_pow]
have prop :
(fun n : ℕ => p ^ n • x = 0) = fun n : ℕ => (Associates.mk <| generator <| torsionOf R M x) ∣ Associates.mk p ^ n :=
by ext n; rw [← Associates.mk_pow, Associates.mk_dvd_mk, ← mem_iff_generator_dvd]; rfl
have := (isTorsion'_powers_iff p).mp hM x; rw [prop] at this
convert Associates.eq_pow_find_of_dvd_irreducible_pow (Associates.irreducible_mk.mpr hp) this.choose_spec
