rpow_rpow_inv

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#ENNReal.rpow_rpow_inv

English

For any y ≠ 0, (x^y)^{y^{-1}} = x.

Русский

Для любого y ≠ 0, (x^y)^{y^{-1}} = x.

LaTeX

$$$ (x^{y})^{y^{-1}} = x \\quad (y \\neq 0) $$$

Lean4

@[simp]
theorem rpow_rpow_inv {y : ℝ} (hy : y ≠ 0) (x : ℝ≥0∞) : (x ^ y) ^ y⁻¹ = x := by
  rw [← rpow_mul, mul_inv_cancel₀ hy, rpow_one]

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

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

Разделы

Аффилиация

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