rpow_sub_intCast

Mathlib.Analysis.SpecialFunctions.Pow.Real

URI: https://scilib.ai/kg/mathlib#Real.rpow_sub_intCast

English

Let hx ≠ 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 \\\\neq 0, \\\\forall y \\\\in \\\\mathbb{R}, \\\\forall n \\\\in \\\\mathbb{Z}, \ x^{\, y-n} = \\frac{x^y}{x^n}.$$$

Lean4

theorem rpow_sub_intCast {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℤ) : x ^ (y - n) = x ^ y / x ^ n := by
  simpa using rpow_add_intCast hx y (-n)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru