zpow_lt_zpow_iff_right — Mathlib

English

Let a be an element with 1 < a in an ordered commutative group. Then for all integers m and n, a^m < a^n if and only if m < n.

Русский

Пусть a — элемент так, что 1 < a в упорядоченной коммутативной группе. Тогда для всех целых m и n верно: a^m < a^n тогда и только тогда, когда m < n.

LaTeX

$$$\forall a\, (1 < a) \implies \forall m,n \in \mathbb{Z},\ a^m < a^n \iff m < n$$$

Lean4

@[to_additive zsmul_lt_zsmul_iff_left]
theorem zpow_lt_zpow_iff_right (ha : 1 < a) : a ^ m < a ^ n ↔ m < n :=
  (zpow_right_strictMono ha).lt_iff_lt

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