IsTorsion' — Mathlib

English

The annihilator of M is a set consisting of all a ∈ R with a · x = 0 for all x ∈ M; IsTorsionBySet holds for this set.

Русский

Аннигилятор M — множество всех a ∈ R с условием a · x = 0 для всех x ∈ M; IsTorsionBySet выполняется для этого множества.

LaTeX

$$IsTorsionBySet(R,M, annihilator(R,M))$$

Lean4

/-- An `S`-torsion module is a module where every element is `a`-torsion for some `a` in `S`. -/
abbrev IsTorsion' (S : Type*) [SMul S M] :=
  ∀ ⦃x : M⦄, ∃ a : S, a • x = 0

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