English
If x ≠ 0 and x ≠ ∞, then x^(m+n) = x^m · x^n for integers m, n.
Русский
Если x ≠ 0 и x ≠ ∞, то x^(m+n) = x^m · x^n для целых m, 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$$$
Lean4
protected theorem zpow_add {x : ℝ≥0∞} (hx : x ≠ 0) (h'x : x ≠ ∞) (m n : ℤ) : x ^ (m + n) = x ^ m * x ^ n :=
by
lift x to ℝ≥0 using h'x
replace hx : x ≠ 0 := by simpa only [Ne, coe_eq_zero] using hx
simp only [← coe_zpow hx, zpow_add₀ hx, coe_mul]