one_lt_zpow_iff_right₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#one_lt_zpow_iff_right₀

English

For a > 1, 1 < a^n iff 0 < n.

Русский

Для a > 1, 1 < a^n тогда и только тогда, когда 0 < n.

LaTeX

$$$1 < a \implies 1 < a^{n} \iff 0 < n$$$

Lean4

@[simp]
theorem one_lt_zpow_iff_right₀ (ha : 1 < a) : 1 < a ^ n ↔ 0 < n := by simp [← zpow_lt_zpow_iff_right₀ ha]

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

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

Разделы

Аффилиация

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