pow_inj_iff_of_orderOf_eq_zero

Mathlib.GroupTheory.OrderOfElement

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

← MathLib Explorer

English

If orderOf x equals 0, then x^n = x^m iff n = m.

Русский

Если orderOf(x) = 0, то x^n = x^m эквивалентно n = m.

LaTeX

$$orderOf(x) = 0 \Rightarrow (x^n = x^m \iff n = m)$$

Lean4

@[to_additive]
theorem pow_inj_iff_of_orderOf_eq_zero (h : orderOf x = 0) {n m : ℕ} : x ^ n = x ^ m ↔ n = m := by
  rw [pow_eq_pow_iff_modEq, h, modEq_zero_iff]

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

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

Разделы

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

Аффилиация

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