div_rpow_of_nonneg

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

← MathLib Explorer

English

For x ∈ ENNReal and y ∈ ℝ, hPow and inv commute in the sense that (x^{-1})^y = (x^y)^{-1}.

Русский

Для x ∈ ENNReal и y ∈ ℝ выполняется (x^{-1})^y = (x^y)^{-1}.

LaTeX

$$$$(x^{-1})^{y} = (x^{y})^{-1}$$$$

Lean4

theorem div_rpow_of_nonneg (x y : ℝ≥0∞) {z : ℝ} (hz : 0 ≤ z) : (x / y) ^ z = x ^ z / y ^ z := by
  rw [div_eq_mul_inv, mul_rpow_of_nonneg _ _ hz, inv_rpow, div_eq_mul_inv]

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

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

Разделы

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

Аффилиация

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