zpow_right_strictMono — Mathlib

English

If a > 1 in a commutative group with a partial order and IsOrderedMonoid, then the map n ↦ a^n is strictly monotone on ℤ.

Русский

Если a > 1 в коммуттивной группе с порядком и IsOrderedMonoid, то функция n ↦ a^n строго монотонна на множестве целых чисел.

LaTeX

$$$ [CommGroup \\alpha] [PartialOrder \\alpha] [IsOrderedMonoid \\alpha] {a : \\alpha}, a > 1 \\Rightarrow \\text{StrictMono}(n \\mapsto a^n). $$$

Lean4

@[to_additive zsmul_left_strictMono]
theorem zpow_right_strictMono (ha : 1 < a) : StrictMono fun n : ℤ ↦ a ^ n :=
  by
  refine strictMono_int_of_lt_succ fun n ↦ ?_
  rw [zpow_add_one]
  exact lt_mul_of_one_lt_right' (a ^ n) ha

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