le_self_pow

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

URI: https://scilib.ai/kg/mathlib#le_self_pow

English

If a ≥ 1 and n ≠ 0, then a ≤ a^n.

Русский

Если a ≥ 1 и n ≠ 0, то a ≤ a^n.

LaTeX

$$$ 1 \le a \Rightarrow n \neq 0 \Rightarrow a \le a^n $$$

Lean4

@[to_additive]
theorem le_self_pow (ha : 1 ≤ a) (hn : n ≠ 0) : a ≤ a ^ n := by
  simpa using pow_le_pow_right' ha (Nat.one_le_iff_ne_zero.2 hn)

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

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

Разделы

Аффилиация

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