pow_pos

Mathlib.Algebra.Order.Ring.Canonical

URI: https://scilib.ai/kg/mathlib#CanonicallyOrderedAdd.pow_pos

English

For odd n, a^n ≤ b^n iff a ≤ b.

Русский

Для нечетного n, a^n ≤ b^n эквивалентно a ≤ b.

LaTeX

$$$a^n \le b^n \iff a \le b$$$

Lean4

theorem pow_pos [NoZeroDivisors R] {a : R} (ha : 0 < a) (n : ℕ) : 0 < a ^ n :=
  pos_iff_ne_zero.2 <| pow_ne_zero _ ha.ne'

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

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

Разделы

Аффилиация

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