neg_one_ne_one

Mathlib.Data.ZMod.Basic

URI: https://scilib.ai/kg/mathlib#ZMod.neg_one_ne_one

English

In ZMod n with n > 2, the element −1 is not equal to 1.

Русский

В ZMod n при n > 2 элемент −1 не равен 1.

LaTeX

$$$(-1) \neq 1 \quad \text{если } 2 < n$$$

Lean4

theorem neg_one_ne_one {n : ℕ} [Fact (2 < n)] : (-1 : ZMod n) ≠ 1 :=
  CharP.neg_one_ne_one (ZMod n) n

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

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

Разделы

Аффилиация

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