rpow_add_intCast — Mathlib

English

Let x ≥ 0, y ∈ ℝ, and n ∈ ℤ. Then x^{y+n} = x^y · x^n.

Русский

Пусть x ≥ 0, y ∈ ℝ и n ∈ ℤ. Тогда x^{y+n} = x^y · x^n.

LaTeX

$$$\\\\forall x \\\\ge 0, \\\\forall y \\\\in \\\\mathbb{R}, \\\\forall n \\\\in \\\\mathbb{Z}, \ x^{\, y+n} = x^y \cdot x^n.$$$

Lean4

theorem rpow_add_intCast {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℤ) : x ^ (y + n) = x ^ y * x ^ n := by
  rw [rpow_def, rpow_def, Complex.ofReal_add, Complex.cpow_add _ _ (Complex.ofReal_ne_zero.mpr hx),
    Complex.ofReal_intCast, Complex.cpow_intCast, ← Complex.ofReal_zpow, mul_comm, Complex.re_ofReal_mul, mul_comm]

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