div_rpow

Mathlib.Analysis.SpecialFunctions.Pow.Real

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

← MathLib Explorer

English

Let x ≥ 0, y ≥ 0. Then (x / y)^z = x^z / y^z for z ∈ ℝ.

Русский

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

LaTeX

$$$\\\\forall x \\\\ge 0, \\\\forall y \\\\ge 0, \\\\forall z: \ (x / y)^z = x^z / y^z.$$$

Lean4

theorem div_rpow (hx : 0 ≤ x) (hy : 0 ≤ y) (z : ℝ) : (x / y) ^ z = x ^ z / y ^ z := by
  simp only [div_eq_mul_inv, mul_rpow hx (inv_nonneg.2 hy), inv_rpow hy]

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

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

Разделы

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

Аффилиация

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