neg — Mathlib

English

For any additive abelian group A and integer n, the n-torsion subgroup satisfies A[-n] = A[n], i.e., negation of the index does not change the torsion subgroup.

Русский

Для любой аддитивной абелевой группы A и целого числа n выполняется A[-n] = A[n], то есть замена n на -n не меняет торионную подпмодуль.

LaTeX

$$$A[-n] = A[n]$$$

Lean4

theorem neg : A[-n] = A[n] := by
  ext a
  simp

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