rpow_inv_natCast_pow — Mathlib

English

Let n ≠ 0 in ℕ and x ∈ ℝ≥0∞. Then (x^(1/n))^n = x.

Русский

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

LaTeX

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

Lean4

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

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