English
For r ≠ 0, and any integer n, (↑(r^n) : ENNReal) = (r : ENNReal)^n.
Русский
Пусть r ≠ 0. Тогда для любого целого n выполняется (↑(r^n) : ENNReal) = (r : ENNReal)^n.
LaTeX
$$$\\forall r \\in \\mathbb{R}_{\\ge 0},\\ r \\neq 0 \\Rightarrow \\forall n \\in \\mathbb{Z}, \\; (↑(r^n) : \\mathbb{R}_{\\ge 0}^{\\infty}) = (r : \\mathbb{R}_{\\ge 0}^{\\infty})^n$$$
Lean4
@[simp, norm_cast]
theorem coe_zpow (hr : r ≠ 0) (n : ℤ) : (↑(r ^ n) : ℝ≥0∞) = (r : ℝ≥0∞) ^ n :=
by
rcases n with n | n
· simp only [Int.ofNat_eq_coe, coe_pow, zpow_natCast]
· have : r ^ n.succ ≠ 0 := pow_ne_zero (n + 1) hr
simp only [zpow_negSucc, coe_inv this, coe_pow]
