sq_ne_one_iff

Mathlib.Algebra.Ring.Commute

URI: https://scilib.ai/kg/mathlib#sq_ne_one_iff

English

In a ring with NoZeroDivisors, a^2 ≠ 1 iff a ≠ 1 and a ≠ −1.

Русский

В кольце без нулевых делителей, если a^2 ≠ 1, то a ≠ 1 и a ≠ −1.

LaTeX

$$$ a^2 \\neq 1 \\iff a \\neq 1 \\land a \\neq -1 $$$

Lean4

theorem sq_ne_one_iff : a ^ 2 ≠ 1 ↔ a ≠ 1 ∧ a ≠ -1 :=
  sq_eq_one_iff.not.trans not_or

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

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

Разделы

Аффилиация

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