rpow_sub

Mathlib.Analysis.SpecialFunctions.Pow.Real

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

← MathLib Explorer

English

If x > 0 and y,z ∈ ℝ, then x^(y−z) = x^y / x^z.

Русский

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

LaTeX

$$$x > 0 \Rightarrow ∀ y,z \in \mathbb{R},\ x^{y-z} = x^{y} / x^{z}$$$

Lean4

theorem rpow_sub {x : ℝ} (hx : 0 < x) (y z : ℝ) : x ^ (y - z) = x ^ y / x ^ z := by
  simp only [sub_eq_add_neg, rpow_add hx, rpow_neg (le_of_lt hx), div_eq_mul_inv]

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

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

Разделы

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

Аффилиация

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