zpow_le_zpow_right₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

If a ≥ 1 and m ≤ n are integers, then a^m ≤ a^n.

Русский

Если a ≥ 1 и целые числа m ≤ n, то a^m ≤ a^n.

LaTeX

$$$1 \le a \quad\land\quad m \le n\quad\Rightarrow\quad a^{m} \le a^{n}$$$

Lean4

@[gcongr]
theorem zpow_le_zpow_right₀ (ha : 1 ≤ a) (hmn : m ≤ n) : a ^ m ≤ a ^ n :=
  zpow_right_mono₀ ha hmn

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

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

Разделы

Аффилиация

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