zpow_sub — Mathlib

English

For x ≠ 0 and x ≠ ∞, and integers m,n, x^(m−n) = x^m · (x^n)⁻¹.

Русский

Пусть x ≠ 0 и x ≠ ∞. Тогда для целых m,n выполняется x^(m−n) = x^m · (x^n)⁻¹.

LaTeX

$$$\\forall x \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; x \\neq 0 \\land x \\neq \\infty \\Rightarrow \\forall m,n \\in \\mathbb{Z},\\; x^{(m-n)} = x^m \\cdot (x^n)^{-1}$$$

Lean4

protected theorem zpow_sub {x : ℝ≥0∞} (x_ne_zero : x ≠ 0) (x_ne_top : x ≠ ⊤) (m n : ℤ) :
    x ^ (m - n) = (x ^ m) * (x ^ n)⁻¹ := by rw [sub_eq_add_neg, ENNReal.zpow_add x_ne_zero x_ne_top, ENNReal.zpow_neg]

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