nsmul

Mathlib.Algebra.Module.Torsion

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

English

If x ∈ A[n], then n·x = 0; in particular, every element of the n-torsion subgroup is annihilated by n.

Русский

Если x ∈ A[n], то n·x = 0; каждый элемент n-торсионной подпгруппы аннигилируется на n.

LaTeX

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

Lean4

@[simp]
theorem nsmul (x : A[n]) : n • x = 0 :=
  Nat.cast_smul_eq_nsmul ℤ n x ▸ Submodule.smul_torsionBy ..

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

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

Разделы

Аффилиация

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