orderOf_neg_one — Mathlib

English

The order of −1 in a ring depends on the ring's characteristic: it is 1 if the ring has characteristic 2, and 2 otherwise.

Русский

Порядок −1 в кольце равен 1 при характеристике кольца 2 и равен 2 иначе.

LaTeX

$$orderOf(-1) = \\operatorname{ite}(\\operatorname{ringChar}(R) = 2, 1, 2)$$

Lean4

@[simp]
theorem orderOf_neg_one [Nontrivial R] : orderOf (-1 : R) = if ringChar R = 2 then 1 else 2 :=
  by
  split_ifs with h
  · rw [neg_one_eq_one_iff.2 h, orderOf_one]
  apply orderOf_eq_prime
  · simp
  simpa [neg_one_eq_one_iff] using h

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