neg_one_mem_torsion — Mathlib

English

In any commutative monoid equipped with a distributive negation, the element -1 has finite order. Indeed, (-1)^2 = 1, so -1 lies in the torsion subset of the monoid.

Русский

В любом коммутативном моноиде с распределённым отрицанием элемент -1 имеет конечный порядок. Доказательство: (-1)^2 = 1, следовательно, -1 принадлежит торсионной части моноида.

LaTeX

$$$\exists n \in \mathbb{N}_{>0}: (-1)^n = 1$$$

Lean4

theorem neg_one_mem_torsion : -1 ∈ CommMonoid.torsion M :=
  ⟨2, zero_lt_two, (isPeriodicPt_mul_iff_pow_eq_one _).mpr (by simp)⟩

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