mem_torsion'_iff — Mathlib

English

For S with an S-action, membership of x in torsion'_S M is equivalent to the existence of some a in S with a acting zero on x.

Русский

Для S с действием на M равносильно: x ∈ torsion'_S M тогда и только тогда, когда существует a ∈ S такое, что a · x = 0.

LaTeX

$$x ∈ torsion'_S M ⇔ ∃ a ∈ S, a • x = 0.$$

Lean4

@[simp]
theorem mem_torsion'_iff (x : M) : x ∈ torsion' R M S ↔ ∃ a : S, a • x = 0 :=
  Iff.rfl

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