torsion

Mathlib.Algebra.Module.Torsion

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

← MathLib Explorer

English

The torsion of the zero element is the whole ring, since every scalar kills 0.

Русский

Торсион нуля — это весь кольцо, так как каждый скаляр умножением на 0 даёт 0.

LaTeX

$$$\operatorname{torsionOf}(R,M,0) = \top$$$

Lean4

/-- The torsion submodule, containing all elements `x` of `M` such that `a • x = 0` for some
  non-zero-divisor `a` in `R`. -/
abbrev torsion :=
  torsion' R M R⁰

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

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

Разделы

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

Аффилиация

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