inv_zpow'

Mathlib.Data.ENNReal.Inv

URI: https://scilib.ai/kg/mathlib#ENNReal.inv_zpow'

English

For x ∈ ENNReal and integer n, x⁻¹ ^ n = x ^ (−n).

Русский

Пусть x ∈ ENNReal и целое n. Тогда x⁻¹ ^ n = x^(−n).

LaTeX

$$$\\forall x \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; \\forall n \\in \\mathbb{Z},\\; x^{-1}^{\,n} = x^{-n}$$$

Lean4

protected theorem inv_zpow' (x : ℝ≥0∞) (n : ℤ) : x⁻¹ ^ n = x ^ (-n) := by rw [ENNReal.zpow_neg, ENNReal.inv_zpow]

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

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

Разделы

Аффилиация

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