English
For a module M over a semiring R and a fixed x ∈ M, the torsionOf is the set of scalars a ∈ R such that a · x = 0; this set is an ideal of R.
Русский
Для модуля M над полукольцом R фиксируем x ∈ M. Торсионный идеал torsionOf состоит из всех скаляров a ∈ R, таких что a · x = 0; это идеал в R.
LaTeX
$$$\operatorname{torsionOf}(R,M,x) = \{a \in R \mid a \cdot x = 0\}$$$
Lean4
/-- The torsion ideal of `x`, containing all `a` such that `a • x = 0`. -/
@[simps!]
def torsionOf (x : M) : Ideal R :=
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation on LinearMap.ker https://github.com/leanprover/lean4/issues/1629
LinearMap.ker (LinearMap.toSpanSingleton R M x)
