div_rpow

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#NNReal.div_rpow

English

Let x > 0, y > 0, and z ∈ ℝ. Then (x/y)^z = x^z / y^z.

Русский

Пусть x > 0, y > 0 и z ∈ ℝ. Тогда (x/y)^z = x^z / y^z.

LaTeX

$$x > 0 \land y > 0 \land z \in \mathbb{R} \Rightarrow (\tfrac{x}{y})^{z} = \tfrac{x^{z}}{y^{z}}$$

Lean4

theorem div_rpow (x y : ℝ≥0) (z : ℝ) : (x / y) ^ z = x ^ z / y ^ z :=
  NNReal.eq <| Real.div_rpow x.2 y.2 z

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

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

Разделы

Аффилиация

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