torsion'_torsion'_eq_top

Mathlib.Algebra.Module.Torsion

URI: https://scilib.ai/kg/mathlib#Submodule.torsion'_torsion'_eq_top

English

The torsion submodule of the torsion submodule is the whole torsion submodule.

Русский

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

LaTeX

$$torsion' R (torsion' R M S) S = ⊤$$

Lean4

@[simp]
theorem torsion'_torsion'_eq_top : torsion' R (torsion' R M S) S = ⊤ :=
  (isTorsion'_iff_torsion'_eq_top S).mp <| torsion'_isTorsion' S

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

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

Разделы

Аффилиация

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