rpow_inv_rpow_self

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

English

Let y ≠ 0. Then (x^y)^(1/y) = x for x > 0.

Русский

Пусть y ≠ 0. Тогда (x^y)^(1/y) = x для x > 0.

LaTeX

$$$$ \\forall y\\in\\mathbb{R}\\setminus\\{0\\},\\ \\forall x>0:\\ (x^{\,y})^{\\frac{1}{y}}=x. $$$$

Lean4

theorem rpow_inv_rpow_self {y : ℝ} (hy : y ≠ 0) (x : ℝ≥0) : (x ^ y) ^ (1 / y) = x :=
  by
  rw [← rpow_mul]
  field_simp
  simp

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

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

Разделы

Аффилиация

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