pow_injective

Mathlib.Algebra.Order.Ring.Basic

URI: https://scilib.ai/kg/mathlib#Odd.pow_injective

English

For odd n, the map x → x^n is injective.

Русский

Для нечетного n отображение x → x^n инъективно.

LaTeX

$$$x^n = y^n \implies x = y$ (n odd)$$

Lean4

theorem pow_injective {n : ℕ} (hn : Odd n) : Injective (· ^ n : R → R) :=
  hn.strictMono_pow.injective

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

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

Разделы

Аффилиация

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