rpow_self_rpow_inv

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

English

Let x ≥ 0 and y ≠ 0. Then (x^(1/y))^y = x.

Русский

Пусть x ≥ 0 и y ≠ 0. Тогда (x^{1/y})^y = x.

LaTeX

$$$x \ge 0 \land y \neq 0 \Rightarrow (x^{1/y})^{\,y} = x$$$

Lean4

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

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

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

Разделы

Аффилиация

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