torsionBySet — Mathlib

English

The S-torsion by a set s ⊆ R is the intersection of the a-torsion submodules over all a ∈ image(s); equivalently, it contains those x ∈ M that are annihilated by every a ∈ s.

Русский

Подмодуль S-торсион по множеству s ⊆ R равен пересечению подмодулей по всем a ∈ s; тож это те элементы x ∈ M, которых убивает каждый a ∈ s.

LaTeX

$$torsionBySet(R,M,s) = sInf (torsionBy(R,M,·) '' s)$$

Lean4

/-- The submodule containing all elements `x` of `M` such that `a • x = 0` for all `a` in `s`. -/
@[simps!]
def torsionBySet (s : Set R) : Submodule R M :=
  sInf (torsionBy R M '' s)

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