nsmul_iff

Mathlib.Algebra.Module.Torsion

URI: https://scilib.ai/kg/mathlib#AddSubgroup.torsionBy.nsmul_iff

English

For x ∈ A and n ∈ ℕ, x ∈ A[n] if and only if n·x = 0; i.e., membership in the n-torsion subgroup is equivalent to being annihilated by n.

Русский

Для x ∈ A и n ∈ ℕ: x ∈ A[n] тогда и только тогда, когда n·x = 0.

LaTeX

$$$x \\in A[n] \\iff n\\cdot x = 0$$$

Lean4

theorem nsmul_iff {x : A} : x ∈ A[n] ↔ n • x = 0 :=
  Nat.cast_smul_eq_nsmul ℤ n x ▸ Submodule.mem_torsionBy_iff ..

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

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

Разделы

Аффилиация

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