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})^{-1}$$$

Lean4

protected theorem inv_zpow (x : ℝ≥0∞) (n : ℤ) : x⁻¹ ^ n = (x ^ n)⁻¹ := by cases n <;> simp [ENNReal.inv_pow]

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

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

Разделы

Аффилиация

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