orderOf_abs_ne_one — Mathlib

English

If the absolute value of x is not 1 in a ordered ring, then orderOf x = 0.

Русский

Если abs(x) не равно 1 в упорядоченной кольцевой структуре, то orderOf(x) = 0.

LaTeX

$$orderOf x = 0$$

Lean4

theorem orderOf_abs_ne_one (h : |x| ≠ 1) : orderOf x = 0 :=
  by
  rw [orderOf_eq_zero_iff']
  intro n hn hx
  replace hx : |x| ^ n = 1 := by simpa only [abs_one, abs_pow] using congr_arg abs hx
  rcases h.lt_or_gt with h | h
  · exact ((pow_lt_one₀ (abs_nonneg x) h hn.ne').ne hx).elim
  · exact ((one_lt_pow₀ h hn.ne').ne' hx).elim

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