mem_torsionOf_iff

Mathlib.Algebra.Module.Torsion

URI: https://scilib.ai/kg/mathlib#Ideal.mem_torsionOf_iff

English

For any a ∈ R and x ∈ M, a belongs to the torsionOf of x if and only if a · x = 0.

Русский

Для любых a ∈ R и x ∈ M верно: a принадлежит торсионному идеалу x тогда и только тогда, когда a · x = 0.

LaTeX

$$$a \in \operatorname{torsionOf}(R,M,x) \iff a \cdot x = 0$$$

Lean4

@[simp]
theorem mem_torsionOf_iff (x : M) (a : R) : a ∈ torsionOf R M x ↔ a • x = 0 :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru