one_lt_pow_iff

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

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

English

For nonzero n, 1 < x^n iff 1 < x.

Русский

Для ненулевого n верно: 1 < x^n ⇔ 1 < x.

LaTeX

$$$ n \neq 0 \Rightarrow (1 < x^n \iff 1 < x) $$$

Lean4

@[to_additive nsmul_pos_iff]
theorem one_lt_pow_iff {x : M} {n : ℕ} (hn : n ≠ 0) : 1 < x ^ n ↔ 1 < x :=
  lt_iff_lt_of_le_iff_le (pow_le_one_iff hn)

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

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

Разделы

Аффилиация

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