pow_rpow_inv_natCast — Mathlib

English

Let n be a nonzero natural number and x a nonnegative extended real. Then (x^n)^(1/n) = x.

Русский

Пусть n ∈ ℕ, n ≠ 0, и x ∈ ℝ≥0∞. Тогда (x^n)^{1/n} = x.

LaTeX

$$$\\\\forall n \\\\in \\\\mathbb{N}, \\\\ n \\\\\\neq 0 \\\\rightarrow \\\\forall x \\\\in \\\\mathbb{R}_{\\\\ge 0}^{\\\\infty}, (x^n)^{n^{-1}} = x.$$$

Lean4

theorem pow_rpow_inv_natCast {n : ℕ} (hn : n ≠ 0) (x : ℝ≥0∞) : (x ^ n) ^ (n⁻¹ : ℝ) = x := by
  rw [← rpow_natCast, ← rpow_mul, mul_inv_cancel₀ (by positivity), rpow_one]

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