orderOf_eq_zero_iff'

Mathlib.GroupTheory.OrderOfElement

URI: https://scilib.ai/kg/mathlib#orderOf_eq_zero_iff'

← MathLib Explorer

English

orderOf x = 0 iff ∀ n > 0, x^n ≠ 1.

Русский

orderOf x = 0 эквивалентно тому, что для всех n>0 x^n ≠ 1.

LaTeX

$$orderOf x = 0 \\iff \\forall n > 0, x^n \\neq 1$$

Lean4

@[to_additive]
theorem orderOf_eq_zero_iff' : orderOf x = 0 ↔ ∀ n : ℕ, 0 < n → x ^ n ≠ 1 := by
  simp_rw [orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one, not_exists, not_and]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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