rpow_add_intCast' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem rpow_add_intCast' (hx : 0 ≤ x) {n : ℤ} (h : y + n ≠ 0) : x ^ (y + n) = x ^ y * x ^ n := by
  rw [rpow_add' hx h, rpow_intCast]

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