zpow_add — Mathlib

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]

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