IsTorsionBySet — Mathlib

English

A module is a-torsion for every a in a set s if and only if every a ∈ s annihilates all elements: ∀ x, ∀ a ∈ s, a · x = 0.

Русский

Модуль является a-торсионным для всех a из множества s ⇔ каждый a ∈ s действует как ноль на все элементы: ∀ x, ∀ a ∈ s, a · x = 0.

LaTeX

$$IsTorsionBySet(R,M,s) := ∀ x ∈ M, ∀ a ∈ s, a · x = 0$$

Lean4

/-- A module where every element is `a`-torsion for all `a` in `s`. -/
abbrev IsTorsionBySet (s : Set R) :=
  ∀ ⦃x : M⦄ ⦃a : s⦄, (a : R) • x = 0

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