isTorsionBy_quotient_element_smul

Mathlib.Algebra.Module.Torsion

URI: https://scilib.ai/kg/mathlib#Module.isTorsionBy_quotient_element_smul

← MathLib Explorer

English

For any r, IsTorsionBy R (M ⧸ r • ⊤) r holds.

Русский

Для любого r верно IsTorsionBy R (M / r • ⊤) r.

LaTeX

$$$IsTorsionBy R (M \\ / \\ r \\cdot \\top) r$$$

Lean4

theorem isTorsionBy_quotient_element_smul : IsTorsionBy R (M ⧸ r • (⊤ : Submodule R M)) r :=
  (isTorsionBy_quotient_iff _ _).mpr (Submodule.smul_mem_pointwise_smul · r ⊤ ⟨⟩)

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

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

Разделы

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

Аффилиация

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