le_self_pow₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$ (1 \\le a) \\land (n \\neq 0) \\Rightarrow a \\le a^n $$$

Lean4

theorem le_self_pow₀ [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) (hn : n ≠ 0) : a ≤ a ^ n := by
  simpa only [pow_one] using pow_le_pow_right₀ ha <| Nat.pos_iff_ne_zero.2 hn

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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