orderOf_eq_two_iff — Mathlib

English

For a ring R with prime p ≠ 2 and CharP R p, for any x ∈ R, orderOf x = 2 iff x = −1.

Русский

Для кольца R с простым p ≠ 2 и CharP R p, для любого x ∈ R, orderOf x = 2 тогда $\Leftrightarrow$ x = −1.

LaTeX

$$orderOf x = 2 \\\\Leftrightarrow x = -1$$

Lean4

theorem orderOf_eq_two_iff [Nontrivial R] [NoZeroDivisors R] (p : ℕ) (hp : p ≠ 2) [CharP R p] {x : R} :
    orderOf x = 2 ↔ x = -1 :=
  by
  simp only [orderOf_eq_prime_iff, sq_eq_one_iff, ne_eq, or_and_right, and_not_self, false_or, and_iff_left_iff_imp]
  rintro rfl
  exact fun h ↦ hp ((ringChar.eq R p) ▸ (neg_one_eq_one_iff.1 h))

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