torsion_torsion_eq_top

Mathlib.Algebra.Module.Torsion

URI: https://scilib.ai/kg/mathlib#Submodule.torsion_torsion_eq_top

← MathLib Explorer

English

Quotienting by the torsion submodule yields a torsion-free module.

Русский

Фактор-модуль по торсионному подмодулю является неторсионным.

LaTeX

$$torsion R (M ⧸ torsion R M) = ⊥$$

Lean4

/-- The torsion submodule of the torsion submodule (viewed as a module) is the full
torsion module. -/
theorem torsion_torsion_eq_top : torsion R (torsion R M) = ⊤ :=
  torsion'_torsion'_eq_top R⁰

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru