English
For a general S acting on M, the S-torsion submodule consists of all x ∈ M for which ∃ a ∈ S with a · x = 0.
Русский
Для общего S, действующего на M, S-торсионный подмодуль состоит из всех x ∈ M таких, что существует a ∈ S, и такое, что a · x = 0.
LaTeX
$$torsion'(R,M,S) = { x ∈ M | ∃ a ∈ S, a · x = 0 }$$
Lean4
/-- The `a`-torsion submodule for `a` in `R`, containing all elements `x` of `M` such that
`a • x = 0`. -/
@[simps!]
def torsionBy (a : R) : Submodule R M :=
-- 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 (DistribMulAction.toLinearMap R M a)
