zpow_lt_zpow_right — Mathlib

English

If 1 < a in a commutative group with a partial order and IsOrderedMonoid, then a^m ≤ a^n iff m ≤ n.

Русский

Если a > 1, то a^m ≤ a^n эквивалентно m ≤ n.

LaTeX

$$$ [CommGroup \\alpha] [PartialOrder \\alpha] [IsOrderedMonoid \\alpha] {m n : \\mathbb{Z}} {a : \\alpha}, a > 1 \\Rightarrow (a^m ≤ a^n) \\iff (m ≤ n). $$$

Lean4

@[to_additive (attr := gcongr) zsmul_lt_zsmul_left]
theorem zpow_lt_zpow_right (ha : 1 < a) (h : m < n) : a ^ m < a ^ n :=
  zpow_right_strictMono ha h

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