English
If x ≥ 0, then (x^n).toNNReal = x.toNNReal^n for all integers n.
Русский
Если x ≥ 0, то (x^n).toNNReal = (x.toNNReal)^n для всех целых n.
LaTeX
$$$$ x \ge 0 \implies (x^n)^{\mathrm{toNNReal}} = (x^{\mathrm{toNNReal}})^n, \quad n \in \mathbb{Z}. $$$$
Lean4
theorem toNNReal_zpow {x : ℝ} (hx : 0 ≤ x) (n : ℤ) : (x ^ n).toNNReal = x.toNNReal ^ n := by
rw [← coe_inj, NNReal.coe_zpow, Real.coe_toNNReal _ (zpow_nonneg hx _), Real.coe_toNNReal x hx]