English
For x ∈ ENNReal and m ∈ ℤ, x^(−m) = (x^m)⁻¹.
Русский
Для x ∈ ENNReal и m ∈ ℤ выполняется x^(−m) = (x^m)⁻¹.
LaTeX
$$$\\forall x \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; \\forall m \\in \\mathbb{Z},\\; x^{(-m)} = (x^m)^{-1}$$$
Lean4
protected theorem zpow_neg (x : ℝ≥0∞) (m : ℤ) : x ^ (-m) = (x ^ m)⁻¹ :=
by
obtain hx₀ | hx₀ := eq_or_ne x 0
· obtain hm | hm | hm := lt_trichotomy m 0 <;> simp_all [zero_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]
obtain hx | hx := eq_or_ne x ⊤
· obtain hm | hm | hm := lt_trichotomy m 0 <;> simp_all [top_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]
exact ENNReal.eq_inv_of_mul_eq_one_left (by simp [← ENNReal.zpow_add hx₀ hx])
