torsionBy_isTorsionBy

Mathlib.Algebra.Module.Torsion

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

English

The a-torsion submodule is itself an a-torsion module.

Русский

Подмодуль a-торсиона является a-торсионным модулем.

LaTeX

$$$IsTorsionBy\,R\,M\,a \Rightarrow IsTorsionBy\,R\, (torsionBy\,R\,M\, a) \, a$$$

Lean4

/-- The `a`-torsion submodule is an `a`-torsion module. -/
theorem torsionBy_isTorsionBy : IsTorsionBy R (torsionBy R M a) a :=
  smul_torsionBy a

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

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

Разделы

Аффилиация

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