rpow_div_two_eq_sqrt

Mathlib.Analysis.SpecialFunctions.Pow.Real

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

English

For x ≥ 0, x^{r/2} = (√x)^r for any real r.

Русский

Для x ≥ 0 верно x^{r/2} = (√x)^r для любого вещественного r.

LaTeX

$$For x ∈ ℝ, r ∈ ℝ, with x ≥ 0: x^{r/2} = (√x)^{r}.$$

Lean4

theorem rpow_div_two_eq_sqrt {x : ℝ} (r : ℝ) (hx : 0 ≤ x) : x ^ (r / 2) = √x ^ r :=
  by
  rw [sqrt_eq_rpow, ← rpow_mul hx]
  congr
  ring

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

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

Разделы

Аффилиация

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