isTorsionBy_iff_mem_annihilator

Mathlib.Algebra.Module.Torsion

URI: https://scilib.ai/kg/mathlib#Module.isTorsionBy_iff_mem_annihilator

English

For a ∈ R, a is a torsion action on M if and only if a is in the annihilator of M.

Русский

Для a ∈ R действие a на M является торсионным тогда и только тогда, когда a лежит в аннигиляторе M.

LaTeX

$$IsTorsionBy(R,M,a) ↔ a ∈ annihilator(R,M)$$

Lean4

theorem isTorsionBy_iff_mem_annihilator {a : R} : IsTorsionBy R M a ↔ a ∈ annihilator R M := by
  rw [IsTorsionBy, mem_annihilator]

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

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

Разделы

Аффилиация

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